mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-26 08:09:22 +03:00
Merge branch 'master' of https://github.com/uwu-tech/Kind
This commit is contained in:
commit
3813a599df
@ -1,3 +1,3 @@
|
||||
Ether.Bits.get_bytes_size(bytes : Bits) : Nat
|
||||
let bytes_size = Bits.length(bytes) / 8
|
||||
if (Nat.mod(Bits.length(bytes), 8)) >? 0 then bytes_size +1 else bytes_size
|
||||
if (Nat.mod(Bits.length(bytes), 8)) >? 0 then bytes_size +1 else Nat.max(1, bytes_size)
|
@ -12,9 +12,10 @@ Ether.RLP.encode.bytes(tree : Ether.RLP.Tree) : List<Bits>
|
||||
for item in tree.value with bytes :
|
||||
bytes ++ Ether.RLP.encode.bytes(item)
|
||||
let bytes_size = List.foldr!!(0, (x, y) Ether.Bits.get_bytes_size(x) + y, bytes)
|
||||
log("first encoding " | Nat.show(bytes_size))
|
||||
Ether.RPL.encode_length(bytes_size, 192) ++ bytes
|
||||
}
|
||||
|
||||
//56 +
|
||||
Ether.RPL.encode_length(value : Nat, offSet : Nat) : List<Bits>
|
||||
switch(Nat.ltn(value)) {
|
||||
56 :
|
||||
@ -22,6 +23,8 @@ Ether.RPL.encode_length(value : Nat, offSet : Nat) : List<Bits>
|
||||
18446744073709551616 :
|
||||
let binary_encoding = Ether.RPL.encode.binary(value)
|
||||
let len = List.foldr!!(0, (x, y) Ether.Bits.get_bytes_size(x) + y, binary_encoding)
|
||||
log(Nat.show(value) | " " | Bits.show(List.foldr!!(Bits.e, Bits.concat, [Nat.to_bits(len + offSet + 55)] ++ binary_encoding)))
|
||||
|
||||
[Nat.to_bits(len + offSet + 55)] ++ binary_encoding
|
||||
} default [] // This case has to be treated within a proof
|
||||
|
||||
|
72
base/Ether/RLP/proof/encode.kind
Normal file
72
base/Ether/RLP/proof/encode.kind
Normal file
@ -0,0 +1,72 @@
|
||||
Bits.concat.go(a: Bits, b: Bits): Bits
|
||||
case a {
|
||||
e: b,
|
||||
o: Bits.concat(a.pred, Bits.o(b))
|
||||
i: Bits.concat(a.pred, Bits.i(b))
|
||||
}
|
||||
|
||||
Ether.RLP.proof.encode.bytes(tree : Ether.RLP.Tree) : Bits
|
||||
case tree {
|
||||
tip :
|
||||
let bytes_size = Ether.Bits.get_bytes_size(tree.value)
|
||||
// let u16_char = Bits.trim(4, tree.value)
|
||||
if (bytes_size =? 1) && Bits.ltn(tree.value, Ether.RLP.Constants.bits_128) then
|
||||
tree.value
|
||||
else
|
||||
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 128), tree.value)
|
||||
list :
|
||||
let bytes = Bits.e
|
||||
for item in tree.value with bytes :
|
||||
Bits.concat(bytes, Ether.RLP.proof.encode.bytes(item))
|
||||
let bytes_size = Ether.Bits.get_bytes_size(bytes)
|
||||
log("Second encoding " | Nat.show(bytes_size))
|
||||
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 192), bytes)
|
||||
}
|
||||
|
||||
Ether.RPL.proof.encode_length(value : Nat, offSet : Nat) : Bits
|
||||
switch(Nat.ltn(value)) {
|
||||
56 :
|
||||
Nat.to_bits(value + offSet)
|
||||
} default
|
||||
let binary_encoding = Ether.RPL.proof.encode.binary(value)
|
||||
let len = Ether.Bits.get_bytes_size(binary_encoding)
|
||||
log(Nat.show(value) | " " | Bits.show(Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)))
|
||||
Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)
|
||||
|
||||
Ether.RPL.proof.encode.binary(value : Nat) : Bits
|
||||
if (value =? 0) then
|
||||
Bits.e
|
||||
else
|
||||
Bits.concat.go(Ether.RPL.proof.encode.binary(value / 256), Nat.to_bits(value % 256))
|
||||
|
||||
Bits.break(len : Nat, bits : Bits) : Pair<Bits, Bits>
|
||||
{Bits.take(len, bits), Bits.drop(len, bits)}
|
||||
|
||||
Ether.RLP.proof.encode.read.binary(value : Bits) : Nat
|
||||
let {head, rest} = Bits.break(8, value)
|
||||
let decode = Bits.to_nat(head)
|
||||
if (Bits.eql(rest, Bits.o(Bits.e))) then
|
||||
decode
|
||||
else
|
||||
Ether.RLP.proof.encode.read.binary(rest) + (decode * 256)
|
||||
|
||||
Ether.RLP.proof.encode.read(bits : Bits) : String
|
||||
let {byte_prefix, rest} = Bits.break(8, bits)
|
||||
"0x" | switch (Bits.ltn(byte_prefix)) {
|
||||
Ether.RLP.Constants.bits_128 :
|
||||
String.reverse(Bits.hex.encode(bits)) // between (0, 127)
|
||||
Ether.RLP.Constants.bits_184 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 128) * 8
|
||||
let {prefix, rest} = Bits.break(content_length, rest)
|
||||
String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(prefix))
|
||||
Ether.RLP.Constants.bits_192 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 183) * 8
|
||||
let {head, rest} = Bits.break(content_length, rest)
|
||||
let length = Ether.RLP.proof.encode.read.binary(head)
|
||||
let {prefix, rest} = Bits.break(length*8, rest)
|
||||
String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(head))
|
||||
| String.reverse(Bits.hex.encode(prefix))
|
||||
|
||||
// {Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
|
||||
|
||||
} default ""
|
@ -1,21 +1,55 @@
|
||||
bool_dec(b : Bool, b2 : Bool) : Decidable<b == b2>
|
||||
case b {
|
||||
true : case b2 {
|
||||
true : Decidable.yep!(refl)
|
||||
false : Decidable.nop!((H) Bool.false_neq_true(mirror(H)))
|
||||
}!
|
||||
false : case b2 {
|
||||
true : Decidable.nop!(Bool.false_neq_true)
|
||||
false : Decidable.yep!(refl)
|
||||
}!
|
||||
Bool.and.eq_sym(x : Bool, y : Bool, H : Equal(Bool, Bool.and(x, y), true)) : Pair<x == true, y == true>
|
||||
case x y with H {
|
||||
true true : {refl, refl}
|
||||
false false :
|
||||
def H = Bool.false_neq_true(H)
|
||||
Empty.absurd!(H)
|
||||
true false :
|
||||
def H = Bool.false_neq_true(H)
|
||||
Empty.absurd!(H)
|
||||
false true :
|
||||
def H = Bool.false_neq_true(H)
|
||||
Empty.absurd!(H)
|
||||
}!
|
||||
|
||||
|
||||
Ether.RLP.section(tree : Ether.RLP.Tree) : Equal(Ether.RLP.Tree, Ether.RLP.decode(Ether.RLP.encode(tree)), tree)
|
||||
case tree {
|
||||
tip:
|
||||
?a ::
|
||||
Equal(Ether.RLP.Tree, Ether.RLP.decode(Ether.Bits.read_bytes(Ether.RLP.encode.bytes(Ether.RLP.Tree.tip(tree.value)))),
|
||||
Ether.RLP.Tree.tip(tree.value))
|
||||
let e = refl :: Ether.Bits.read_bytes(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() List(Bits),List.cons(Bits,tree.value,List.nil(Bits)),List.concat(Bits,Ether.RPL.encode_length(Ether.Bits.get_bytes_size(tree.value),128),List.cons(Bits,tree.value,List.nil(Bits))))) == Ether.RLP.encode(Ether.RLP.Tree.tip(tree.value))
|
||||
case e {
|
||||
refl:
|
||||
let remember = case Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)) {
|
||||
true : (H)
|
||||
let {bite_size_cond, bits_ltn_cond} = Bool.and.eq_sym!!(mirror(H))
|
||||
?ak-142-2
|
||||
false : ?bk
|
||||
} : Equal(Bool, self, Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), Bits.ltn(tree.value,Ether.RLP.Constants.bits_128))) -> Ether.RLP.decode(Ether.Bits.read_bytes(self(() List(Bits),List.cons(Bits,tree.value,List.nil(Bits)),List.concat(Bits,Ether.RPL.encode_length(Ether.Bits.get_bytes_size(tree.value),128),List.cons(Bits,tree.value,List.nil(Bits)))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
remember(refl)
|
||||
// case remember.fst with remember.snd {
|
||||
// true : ?a
|
||||
// false : ?b
|
||||
// } : Ether.RLP.decode(Ether.Bits.read_bytes(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() List(Bits),List.cons(Bits,tree.value,List.nil(Bits)),List.concat(Bits,Ether.RPL.encode_length(Ether.Bits.get_bytes_size(tree.value),128),List.cons(Bits,tree.value,List.nil(Bits)))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
//let remember_eq = refl :: Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)) == eq
|
||||
//case Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)) with remember_eq {
|
||||
// true : ?a
|
||||
//false : ?b
|
||||
//}!
|
||||
} : Ether.RLP.decode(e.b) == Ether.RLP.Tree.tip(tree.value)
|
||||
|
||||
// case Nat.eql(Ether.Bits.get_bytes_size(tree.value),1) as eq {
|
||||
// true: ?a
|
||||
// false: ?b
|
||||
//}: Ether.RLP.decode(Ether.Bits.read_bytes(Bool.and(eq,Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() List(Bits),List.cons(Bits,tree.value,List.nil(Bits)),List.concat(Bits,Ether.RPL.encode_length(Ether.Bits.get_bytes_size(tree.value),128),List.cons(Bits,tree.value,List.nil(Bits)))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
//}: Ether.RLP.decode(e.b) == Ether.RLP.Tree.tip(tree.value)
|
||||
|
||||
// case e {
|
||||
// refl:
|
||||
// case Nat.eql(Ether.Bits.get_bytes_size(tree.value),1) as eq {
|
||||
// true: ?a
|
||||
// false: ?b
|
||||
//}: Ether.RLP.decode(Ether.Bits.read_bytes(Bool.and(eq,Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() List(Bits),List.cons(Bits,tree.value,List.nil(Bits)),List.concat(Bits,Ether.RPL.encode_length(Ether.Bits.get_bytes_size(tree.value),128),List.cons(Bits,tree.value,List.nil(Bits)))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
//}: Ether.RLP.decode(e.b) == Ether.RLP.Tree.tip(tree.value)
|
||||
list:
|
||||
?b
|
||||
}!
|
||||
?list_goal
|
||||
} : Equal(Ether.RLP.Tree, Ether.RLP.decode(Ether.RLP.encode(tree)), tree)
|
2082
base/Ether/test.js
Normal file
2082
base/Ether/test.js
Normal file
File diff suppressed because one or more lines are too long
@ -1,8 +1,23 @@
|
||||
Ether.tests : _
|
||||
let ab = Bits.read("10101010")
|
||||
log(String.from_list(Ether.Base.X64.encode(ab)))
|
||||
Ether.Base.X64.decode(Ether.Base.X64.encode(ab))
|
||||
Bits.concat.go(a: Bits, b: Bits): Bits
|
||||
case a {
|
||||
e: b,
|
||||
o: Bits.concat(a.pred, Bits.o(b))
|
||||
i: Bits.concat(a.pred, Bits.i(b))
|
||||
}
|
||||
|
||||
Ether.tests : _
|
||||
//let v = Ether.RLP.Tree.list(
|
||||
// [
|
||||
// Ether.RLP.Tree.tip(Bits.read(String.reverse("1000111011111010110"))),
|
||||
// Ether.RLP.Tree.tip(Bits.read(String.reverse("1000111011111010110")))
|
||||
// ])
|
||||
let v = Ether.RLP.Tree.tip(Bits.read("1000000100000000000000000110110000000000000000000010000000000000000011011000111111111111111111111111111111111011111000000000000100011111111111111111111111111111111101111100000000000000000000000000000001000000000000000001101100100011111111111111111111111111111111101111100000000000010001111111111111111111111111111111110111110000000000000000000000000000000100000000000000000110110000000000000000000010000000000000000011011000000000000000000010110110"))
|
||||
let test1 = Ether.RLP.proof.encode.bytes(v)
|
||||
let test2 = Ether.RLP.encode.bytes(v)
|
||||
log(Ether.RLP.proof.encode.read(test1))
|
||||
log(Ether.RLP.encode.read(test2))
|
||||
let test2 = List.foldr!!(Bits.e, Bits.concat.go, test2)
|
||||
{test1, test2}
|
||||
//let buffer = Buffer8.from_hex("d69429d7d1dd5b6f9c864d9db560d72a247c178ae86b0a")
|
||||
//let hash = Crypto.Keccak.hash.bytes(buffer)
|
||||
//Buffer8.to_hex(hash)
|
@ -3,7 +3,7 @@
|
||||
|
||||
// TODO:
|
||||
// - merge type-checking and validation / allow reusing word terms
|
||||
// - cost measure
|
||||
// - cost measure, WIP rígille
|
||||
// - Lit.Core.Term.get_caller ?
|
||||
// - owned types/constructors ?
|
||||
// - conseguir modificar o dono no Lit.Core.Term.bind
|
||||
@ -14,6 +14,7 @@
|
||||
// - paper:
|
||||
// - use railroad diagrams for syntax
|
||||
|
||||
//
|
||||
// Types
|
||||
// -----
|
||||
|
||||
@ -64,7 +65,7 @@ type Lit.Core.Term {
|
||||
// Binds an new program
|
||||
bind(
|
||||
name: String
|
||||
main: Lit.Core.Term
|
||||
main: Lit.Core.Term // TODO rename to `body`
|
||||
cont: Lit.Core.Term
|
||||
)
|
||||
}
|
||||
@ -146,6 +147,34 @@ type Lit.Core.Statement {
|
||||
Lit.Core.Page: Type
|
||||
List<Lit.Core.Statement>
|
||||
|
||||
type Lit.Core.Costs {
|
||||
new(
|
||||
var: Nat
|
||||
create: Nat
|
||||
match: Nat
|
||||
match_substitution: Nat
|
||||
word: Nat
|
||||
compare: Nat
|
||||
operate: Nat
|
||||
call: Nat
|
||||
bind: Nat
|
||||
)
|
||||
}
|
||||
|
||||
Lit.Core.Costs.default: Lit.Core.Costs
|
||||
Lit.Core.Costs.new(
|
||||
Nat.pow(2, 16*0)
|
||||
Nat.pow(2, 16*1)
|
||||
Nat.pow(2, 16*2)
|
||||
Nat.pow(2, 16*3)
|
||||
Nat.pow(2, 16*4)
|
||||
Nat.pow(2, 16*5)
|
||||
Nat.pow(2, 16*6)
|
||||
Nat.pow(2, 16*7)
|
||||
Nat.pow(2, 16*8)
|
||||
)
|
||||
|
||||
//
|
||||
// Getters and Setters
|
||||
// -------------------
|
||||
|
||||
@ -174,6 +203,7 @@ Lit.Core.Type.find_ctor(name: String, type: Lit.Core.Type): Maybe<Pair<Nat,Lit.C
|
||||
List.ifind!((i,f) String.eql(f@name,name), type.constructors)
|
||||
}
|
||||
|
||||
//
|
||||
// Type-Checking
|
||||
// -------------
|
||||
|
||||
@ -183,65 +213,81 @@ Lit.Core.Type.equal(a: Lit.Core.Type, b: Lit.Core.Type): Bool
|
||||
data data: String.eql(a.name, b.name)
|
||||
} default false
|
||||
|
||||
Lit.Core.World.check.term(
|
||||
term: Lit.Core.Term
|
||||
type: Lit.Core.Type
|
||||
context: Map<Lit.Core.Type>
|
||||
type Lit.Core.Check.Context {
|
||||
new(
|
||||
world: Lit.Core.World
|
||||
caller: Maybe<String>
|
||||
variables: Map<Lit.Core.Type>
|
||||
)
|
||||
}
|
||||
|
||||
Lit.Core.Check.Context.from_world(world: Lit.Core.World): Lit.Core.Check.Context
|
||||
Lit.Core.Check.Context.new(world, none, {})
|
||||
|
||||
Lit.Core.Check.Context.add_var(
|
||||
context: Lit.Core.Check.Context
|
||||
name: String
|
||||
type: Lit.Core.Type
|
||||
): Lit.Core.Check.Context
|
||||
open context
|
||||
let new_variables = context.variables{name} <- type
|
||||
Lit.Core.Check.Context.new(context.world, context.caller, new_variables)
|
||||
|
||||
Lit.Core.World.check.term(
|
||||
context: Lit.Core.Check.Context
|
||||
term: Lit.Core.Term
|
||||
type: Lit.Core.Type
|
||||
): Bool
|
||||
// log("- chk: " | Lit.Lang.show.term(term, world) | " : " | Lit.Lang.show.type.short(type)) // DEBUG
|
||||
// log("- ctx: " | String.join(", ", List.map!!((a) a@fst|":"|Lit.Lang.show.type.short(a@snd), Map.to_list!(context)))) // DEBUG
|
||||
// log("- chk: " | Lit.Lang.show.term(term, context@world) | " : " | Lit.Lang.show.type.short(type)) // DEBUG
|
||||
// log("- ctx: " | String.join(", ", List.map!!((a) a@fst|":"|Lit.Lang.show.type.short(a@snd), Map.to_list!(variables)))) // DEBUG
|
||||
// log("") // DEBUG
|
||||
let result = case term {
|
||||
var:
|
||||
// log("-- var " | term.name) // DEBUG
|
||||
let var_type = context{term.name} abort false
|
||||
// log("-- var " | term.name | " " | Lit.Lang.show.type.short(var_type) | " " | Lit.Lang.show.type.short(type)) // DEBUG
|
||||
let var_type = context@variables{term.name} abort false
|
||||
//log("-- var " | term.name | " " | Lit.Lang.show.type.short(var_type) | " " | Lit.Lang.show.type.short(type)) // DEBUG
|
||||
Lit.Core.Type.equal(var_type, type)
|
||||
create:
|
||||
// log("-- create ") // DEBUG
|
||||
let ttyp = Lit.Core.World.get_type(term.type,world) abort false
|
||||
//log("-- create") // DEBUG
|
||||
let ttyp = Lit.Core.World.get_type(term.type, context@world) abort false
|
||||
case ttyp {
|
||||
data:
|
||||
use ctor = ttyp.constructors[term.ctor] abort false
|
||||
let args = Lit.Core.World.check.many(term.vals, List.mapped!(ctor.fields)!((x) x@type), context, world, caller)
|
||||
log(Bool.show(args))
|
||||
log(Bool.show(Lit.Core.Type.equal(ttyp, type)))
|
||||
let args = Lit.Core.World.check.many(context, term.vals, List.mapped!(ctor.fields)!((x) x@type))
|
||||
args && Lit.Core.Type.equal(ttyp, type)
|
||||
} default false
|
||||
call:
|
||||
// log("-- call ") // DEBUG
|
||||
// verify owner
|
||||
let ownr = Lit.Core.World.check.owner(caller, term.func, world)
|
||||
use func = Lit.Core.World.get_func(term.func,world) abort false
|
||||
use otyp = Lit.Core.World.get_type(func.output_type,world) abort false
|
||||
let args = Lit.Core.World.check.many(term.args, func.input_types, context, world, caller)
|
||||
let cont = Lit.Core.World.check.term(term.cont, type, context{term.name} <- otyp, world, caller)
|
||||
let ownr = Lit.Core.World.check.owner(context, term.func)
|
||||
use func = Lit.Core.World.get_func(term.func, context@world) abort false
|
||||
use otyp = Lit.Core.World.get_type(func.output_type, context@world) abort false
|
||||
let args = Lit.Core.World.check.many(context, term.args, func.input_types)
|
||||
let context_new = Lit.Core.Check.Context.add_var(context, term.name, otyp)
|
||||
let cont = Lit.Core.World.check.term(context_new, term.cont, type)
|
||||
ownr && args && cont
|
||||
match:
|
||||
// log("-- match ") // DEBUG
|
||||
let expr_type = Lit.Core.World.get_type(term.type, world) abort false
|
||||
// log("-- match2 ") // DEBUG
|
||||
//log("-- match ") // DEBUG
|
||||
let expr_type = Lit.Core.World.get_type(term.type, context@world) abort false
|
||||
//log("-- match2 ") // DEBUG
|
||||
|
||||
case expr_type {
|
||||
data:
|
||||
let expr = Lit.Core.World.check.term(term.expr, expr_type, context, world, caller)
|
||||
let expr = Lit.Core.World.check.term(context, term.expr, expr_type)
|
||||
let cses = List.mapped!(term.cses)!((x) x@body)
|
||||
let cses = Lit.Core.World.check.match.cases(cses, type, expr_type.constructors, term.name, context, world, caller)
|
||||
let cses = Lit.Core.World.check.match.cases(context, cses, type, expr_type.constructors, term.name)
|
||||
expr && cses
|
||||
} default false
|
||||
bind:
|
||||
// log("-- bind ") // DEBUG
|
||||
// TODO: check access
|
||||
let ownr = Lit.Core.World.check.owner(caller, term.name, world)
|
||||
use func = Lit.Core.World.get_func(term.name,world) abort false
|
||||
use otyp = Lit.Core.World.get_type(func.output_type,world) abort false
|
||||
let nofn = List.is_empty!(func.input_names) // should we allow binds with functions?
|
||||
let main = Lit.Core.World.check.term(term.main, otyp, context, world, caller)
|
||||
let owner_ok = Lit.Core.World.check.owner(context, term.name)
|
||||
use func = Lit.Core.World.get_func(term.name, context@world) abort false
|
||||
use out_type = Lit.Core.World.get_type(func.output_type, context@world) abort false
|
||||
let nofn_ok = List.is_empty!(func.input_names) // TODO: should we allow binds with functions?
|
||||
let main_ok = Lit.Core.World.check.term(context, term.main, out_type)
|
||||
// should the ctx change?
|
||||
let cont = Lit.Core.World.check.term(term.cont, type, context, world, caller)
|
||||
ownr && nofn && main && cont
|
||||
let cont_ok = Lit.Core.World.check.term(context, term.cont, type)
|
||||
owner_ok && nofn_ok && main_ok && cont_ok
|
||||
word:
|
||||
// log("-- word ") // DEBUG
|
||||
case type {
|
||||
@ -251,68 +297,72 @@ Lit.Core.World.check.term(
|
||||
log("not word")
|
||||
false
|
||||
compare:
|
||||
// log("-- compare ") // DEBUG
|
||||
let val0 = Lit.Core.World.check.term(term.val0, Lit.Core.Type.word, context, world, caller)
|
||||
let val1 = Lit.Core.World.check.term(term.val0, Lit.Core.Type.word, context, world, caller)
|
||||
let iflt = Lit.Core.World.check.term(term.iflt, type, context, world, caller)
|
||||
let ifeq = Lit.Core.World.check.term(term.ifeq, type, context, world, caller)
|
||||
let ifgt = Lit.Core.World.check.term(term.ifgt, type, context, world, caller)
|
||||
//log("-- compare ") // DEBUG
|
||||
let val0 = Lit.Core.World.check.term(context, term.val0, Lit.Core.Type.word)
|
||||
let val1 = Lit.Core.World.check.term(context, term.val0, Lit.Core.Type.word)
|
||||
let iflt = Lit.Core.World.check.term(context, term.iflt, type)
|
||||
let ifeq = Lit.Core.World.check.term(context, term.ifeq, type)
|
||||
let ifgt = Lit.Core.World.check.term(context, term.ifgt, type)
|
||||
val0 && val1 && iflt && ifeq && ifgt
|
||||
operate:
|
||||
// log("-- operate ") // DEBUG
|
||||
let val0 = Lit.Core.World.check.term(term.val0, Lit.Core.Type.word, context, world, caller)
|
||||
let val1 = Lit.Core.World.check.term(term.val1, Lit.Core.Type.word, context, world, caller)
|
||||
//log("-- operate ") // DEBUG
|
||||
let val0 = Lit.Core.World.check.term(context, term.val0, Lit.Core.Type.word)
|
||||
let val1 = Lit.Core.World.check.term(context, term.val1, Lit.Core.Type.word)
|
||||
val0 && val1
|
||||
}
|
||||
//log("\n")
|
||||
result
|
||||
|
||||
Lit.Core.World.check.many(
|
||||
context: Lit.Core.Check.Context,
|
||||
terms: List<Lit.Core.Term>
|
||||
types: List<String>
|
||||
context: Map<Lit.Core.Type>
|
||||
world: Lit.Core.World
|
||||
caller: Maybe<String>
|
||||
): Bool
|
||||
open world
|
||||
case terms types {
|
||||
cons cons:
|
||||
let type = Lit.Core.World.get_type(types.head, world) abort false
|
||||
let head = Lit.Core.World.check.term(terms.head, type, context, world, caller)
|
||||
let tail = Lit.Core.World.check.many(terms.tail, types.tail, context, world, caller)
|
||||
let type = Lit.Core.World.get_type(types.head, context@world) abort false
|
||||
let head = Lit.Core.World.check.term(context, terms.head, type)
|
||||
let tail = Lit.Core.World.check.many(context, terms.tail, types.tail)
|
||||
head && tail
|
||||
nil nil:
|
||||
true
|
||||
} default false
|
||||
|
||||
Lit.Core.World.check.match.cases(
|
||||
context: Lit.Core.Check.Context
|
||||
cases: List<Lit.Core.Term>
|
||||
type: Lit.Core.Type
|
||||
ctors: List<Lit.Core.Type.Constructor>
|
||||
name: String
|
||||
context: Map<Lit.Core.Type>
|
||||
world: Lit.Core.World
|
||||
caller: Maybe<String>
|
||||
): Bool
|
||||
open context
|
||||
case cases ctors {
|
||||
cons cons:
|
||||
let ext_context = context
|
||||
for field in ctors.head@fields with ext_context:
|
||||
let type = Lit.Core.World.get_type(field@type, world) <> Lit.Core.Type.data("Empty", [])
|
||||
ext_context{name | "." | field@name} <- type
|
||||
let case_ok = Lit.Core.World.check.term(cases.head, type, ext_context, world, caller)
|
||||
let rest_ok = Lit.Core.World.check.match.cases(cases.tail, type, ctors.tail, name, context, world, caller)
|
||||
let ext_variables = context.variables
|
||||
|
||||
for field in ctors.head@fields with ext_variables:
|
||||
let field_type =
|
||||
Lit.Core.World.get_type(field@type, context.world)
|
||||
<> Lit.Core.Type.data("Empty", [])
|
||||
ext_variables{name | "." | field@name} <- field_type
|
||||
let new_context = Lit.Core.Check.Context.new(
|
||||
context.world
|
||||
context.caller
|
||||
ext_variables
|
||||
)
|
||||
let case_ok = Lit.Core.World.check.term(new_context, cases.head, type)
|
||||
let rest_ok = Lit.Core.World.check.match.cases(new_context, cases.tail, type, ctors.tail, name)
|
||||
case_ok && rest_ok
|
||||
nil nil:
|
||||
true
|
||||
} default false
|
||||
|
||||
Lit.Core.World.check.owner(
|
||||
caller: Maybe<String>
|
||||
context: Lit.Core.Check.Context
|
||||
name: String
|
||||
world: Lit.Core.World
|
||||
): Bool
|
||||
let entry = world{name}
|
||||
open context
|
||||
let entry = context.world{name}
|
||||
case entry {
|
||||
none: false
|
||||
some:
|
||||
@ -323,7 +373,7 @@ Lit.Core.World.check.owner(
|
||||
nil:
|
||||
true
|
||||
cons:
|
||||
case caller {
|
||||
case context.caller as caller {
|
||||
some:
|
||||
if caller.value =? name then
|
||||
true
|
||||
@ -336,109 +386,19 @@ Lit.Core.World.check.owner(
|
||||
} default false
|
||||
}
|
||||
|
||||
// Validation
|
||||
// ----------
|
||||
// Checks if:
|
||||
// - TODO: no global binders with the same name
|
||||
// - variables are used at most once
|
||||
|
||||
// TODO:
|
||||
// - error list
|
||||
|
||||
Lit.Core.validate.term(
|
||||
term: Lit.Core.Term
|
||||
used: Map<Bool>
|
||||
): Pair<Map<Bool>,Bool>
|
||||
Lit.Core.validate.term.aux({used, true}, term)
|
||||
|
||||
Lit.Core.validate.term.aux(
|
||||
state: Pair<Map<Bool>, Bool>
|
||||
term: Lit.Core.Term
|
||||
): Pair<Map<Bool>, Bool>
|
||||
// log( // DEBUG
|
||||
// "- vld: " | Lit.Lang.show.term(term, {}) | " ; "
|
||||
// | "ctx: "
|
||||
// | String.join(
|
||||
// ", ",
|
||||
// List.map!!(
|
||||
// (a) a@fst | ":" | Bool.show(a@snd),
|
||||
// Map.to_list!(state@fst)
|
||||
// )
|
||||
// )
|
||||
// )
|
||||
// log("") // DEBUG
|
||||
|
||||
case term {
|
||||
var:
|
||||
let {used, valid} = state
|
||||
case used{term.name} as was_used {
|
||||
none:
|
||||
// undefined variable
|
||||
{used, false}
|
||||
some:
|
||||
if was_used.value then
|
||||
// variable already used
|
||||
{used, false}
|
||||
else
|
||||
// first use of the variable
|
||||
{used{term.name} <- true, valid}
|
||||
}
|
||||
|
||||
create:
|
||||
for val in term.vals with state:
|
||||
Lit.Core.validate.term.aux(state, val)
|
||||
state
|
||||
|
||||
match:
|
||||
let state = Lit.Core.validate.term.aux(state, term.expr)
|
||||
for cse in term.cses with state:
|
||||
let {fields, _} = cse
|
||||
let field_state = state
|
||||
for field in fields with field_state:
|
||||
let {used, valid} = field_state
|
||||
case used{field} {
|
||||
some:
|
||||
{used, false} // same name used more than once
|
||||
none:
|
||||
{used{field} <- false, valid}
|
||||
}
|
||||
state
|
||||
state
|
||||
|
||||
call:
|
||||
let {used, valid} = state
|
||||
let used = used{term.name} <- false
|
||||
let state = {used, valid}
|
||||
for arg in term.args with state:
|
||||
Lit.Core.validate.term.aux(state, arg)
|
||||
Lit.Core.validate.term.aux(state, term.cont)
|
||||
|
||||
bind:
|
||||
let {used, valid} = state
|
||||
let used = used{term.name} <- false
|
||||
let state = {used, valid}
|
||||
let state = Lit.Core.validate.term.aux(state, term.main)
|
||||
let state = Lit.Core.validate.term.aux(state, term.cont)
|
||||
state
|
||||
|
||||
word:
|
||||
state
|
||||
|
||||
compare:
|
||||
let terms = [term.val0, term.val1, term.iflt, term.ifeq, term.ifgt]
|
||||
for i_term in terms with state:
|
||||
Lit.Core.validate.term.aux(state, i_term)
|
||||
state
|
||||
|
||||
operate:
|
||||
let state = Lit.Core.validate.term.aux(state, term.val0)
|
||||
let state = Lit.Core.validate.term.aux(state, term.val1)
|
||||
state
|
||||
}
|
||||
|
||||
//
|
||||
// Execution
|
||||
// ---------
|
||||
|
||||
//Pair<Lit.Core.Term, Lit.Core.World>
|
||||
type Lit.Core.run.Context {
|
||||
new(
|
||||
term: Lit.Core.Term
|
||||
world: Lit.Core.World
|
||||
gas: Nat
|
||||
)
|
||||
}
|
||||
|
||||
Lit.Core.World.run.page(
|
||||
page: Lit.Core.Page
|
||||
world: Lit.Core.World
|
||||
@ -455,7 +415,6 @@ Lit.Core.World.run.page(
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
Lit.Core.World.run.statement(
|
||||
statement: Lit.Core.Statement
|
||||
world: Lit.Core.World
|
||||
@ -503,19 +462,19 @@ Lit.Core.World.run.statement(
|
||||
some:
|
||||
let otyp = Lit.Core.World.get_type(func.output_type, world)
|
||||
abort log("error: func otyp not found: " | func.name) none
|
||||
let new_context =
|
||||
Lit.Core.Check.Context.new(
|
||||
new_world
|
||||
some(func.name)
|
||||
ctx.value
|
||||
)
|
||||
let term_ok = Lit.Core.World.check.term(
|
||||
func.main,
|
||||
otyp,
|
||||
ctx.value,
|
||||
new_world,
|
||||
some(func.name),
|
||||
new_context
|
||||
func.main
|
||||
otyp
|
||||
)
|
||||
if term_ok then
|
||||
let {_, ok} = Lit.Core.validate.term(func.main, vld)
|
||||
if ok then
|
||||
some(new_world)
|
||||
else
|
||||
log("error: func invalid: " | func.name) none
|
||||
else
|
||||
// log(Lit.Lang.show.type(otyp, world))
|
||||
log("error: func ill-typed: " | func.name) none
|
||||
@ -528,17 +487,16 @@ Lit.Core.World.run.statement(
|
||||
// This assumes that the call returns the built-in type Word to avoid
|
||||
// duplicating the typechecking function.
|
||||
let call_type = Lit.Core.Type.word
|
||||
let term_ok =
|
||||
Lit.Core.World.check.term(exec_term, call_type, {}, world, none)
|
||||
let context = Lit.Core.Check.Context.from_world(world)
|
||||
let term_ok = Lit.Core.World.check.term(context, exec_term, call_type)
|
||||
if term_ok then
|
||||
let {_, ok} = Lit.Core.validate.term(exec_term, {})
|
||||
if ok then
|
||||
let {result, new_world} =
|
||||
Lit.Core.World.run.term(exec_term, world, {})
|
||||
log("- ext_exec: " | Lit.Lang.show.term(result, world))
|
||||
some(new_world)
|
||||
else
|
||||
log("error: exec is invalid") none
|
||||
use ctx =
|
||||
Lit.Core.World.run.term(exec_term, world, {}, 0) // TODO
|
||||
log("- ext_exec: "
|
||||
| Lit.Lang.show.term(ctx.term, world)
|
||||
| " (gas: " | String.pad_left(32, '0', Nat.to_string_base(16, ctx.gas)) | ")"
|
||||
)
|
||||
some(ctx.world)
|
||||
else
|
||||
log("error: exec failed in typecheck") none
|
||||
}
|
||||
@ -549,126 +507,282 @@ Lit.Core.World.run.term(
|
||||
term: Lit.Core.Term
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
// log("- run " | Lit.Lang.show.term(term,world)) // DEBUG
|
||||
// log("- var " | String.join(", ", List.map!!((x) x@fst|":"|Lit.Lang.show.term(x@snd,world), Map.to_list!(vars)))) // DEBUG
|
||||
// log("")
|
||||
case term {
|
||||
var:
|
||||
case vars{term.name} as got {
|
||||
none:
|
||||
{term, world}
|
||||
some:
|
||||
Lit.Core.World.run.term(got.value, world, vars)
|
||||
}
|
||||
log("var!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@var
|
||||
Lit.Core.World.run.term.var(world, vars, term.name, gas)
|
||||
create:
|
||||
let {vals, world} = Lit.Core.World.run.terms(term.vals, world, vars)
|
||||
{Lit.Core.Term.create(term.type, term.ctor, vals), world}
|
||||
log("create!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@create
|
||||
Lit.Core.World.run.term.create(world, vars, term.type, term.ctor, term.vals, gas)
|
||||
match:
|
||||
Maybe {
|
||||
let {expr, world} = Lit.Core.World.run.term(term.expr, world, vars)
|
||||
case expr {
|
||||
create: case term.cses[expr.ctor] as selected_case {
|
||||
some:
|
||||
let {case_fields, case_body} = selected_case.value
|
||||
let vars = for subst in List.zip!!(case_fields, expr.vals):
|
||||
let {field, value} = subst
|
||||
vars{field} <- value
|
||||
Lit.Core.World.run.term(case_body, world, vars)
|
||||
} default {term, world}
|
||||
} default {term,world}
|
||||
}
|
||||
log("match!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@match
|
||||
Lit.Core.World.run.term.match(world, vars, term.name, term.type, term.expr, term.cses, gas)
|
||||
word:
|
||||
{term, world}
|
||||
log("word!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@word
|
||||
{term, world, gas}
|
||||
compare:
|
||||
let {val0, world} = Lit.Core.World.run.term(term.val0, world, vars)
|
||||
let {val1, world} = Lit.Core.World.run.term(term.val1, world, vars)
|
||||
case val0 val1 {
|
||||
word word:
|
||||
case U64.cmp(val0.numb, val1.numb) {
|
||||
ltn:
|
||||
Lit.Core.World.run.term(term.iflt, world, vars)
|
||||
eql:
|
||||
Lit.Core.World.run.term(term.ifeq, world, vars)
|
||||
gtn:
|
||||
Lit.Core.World.run.term(term.ifgt, world, vars)
|
||||
}
|
||||
} default log("error: operands didn't reduce to words") {term, world}
|
||||
log("compare!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@compare
|
||||
Lit.Core.World.run.term.compare(world, vars, term.val0, term.val1, term.iflt, term.ifeq, term.ifgt, gas)
|
||||
operate:
|
||||
let {val0, world} = Lit.Core.World.run.term(term.val0, world, vars)
|
||||
let {val1, world} = Lit.Core.World.run.term(term.val1, world, vars)
|
||||
case val0 val1 {
|
||||
word word:
|
||||
case term.oper {
|
||||
add:
|
||||
{Lit.Core.Term.word(val0.numb + val1.numb), world}
|
||||
sub:
|
||||
{Lit.Core.Term.word(val0.numb - val1.numb), world}
|
||||
mul:
|
||||
{Lit.Core.Term.word(val0.numb * val1.numb), world}
|
||||
div:
|
||||
{Lit.Core.Term.word(val0.numb / val1.numb), world}
|
||||
mod:
|
||||
{Lit.Core.Term.word(val0.numb % val1.numb), world}
|
||||
or:
|
||||
{Lit.Core.Term.word(val0.numb || val1.numb), world}
|
||||
and:
|
||||
{Lit.Core.Term.word(val0.numb && val1.numb), world}
|
||||
xor:
|
||||
{Lit.Core.Term.word(U64.xor(val0.numb, val1.numb)), world}
|
||||
}
|
||||
} default log("error: operand didn't reduce to word") {term, world}
|
||||
log("operate!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@operate
|
||||
Lit.Core.World.run.term.operate(world, vars, term.oper, term.val0, term.val1, gas)
|
||||
call:
|
||||
case world{term.func} as got {
|
||||
none:
|
||||
{term, world}
|
||||
some: case got.value as entry {
|
||||
bond:
|
||||
use func = entry.value
|
||||
let main_vars = vars
|
||||
let state = {main_vars, world}
|
||||
let state = for arg in List.zip!!(func.input_names, term.args):
|
||||
let {main_vars, world} = state
|
||||
let {arg_name, arg_term} = arg
|
||||
let {arg_term, world} = Lit.Core.World.run.term(arg_term, world, main_vars)
|
||||
let main_vars = main_vars{arg_name} <- arg_term
|
||||
{main_vars, world}
|
||||
let {main_vars, world} = state
|
||||
let {done, world} = Lit.Core.World.run.term(func.main, world, main_vars)
|
||||
let vars = vars{term.name} <- done
|
||||
Lit.Core.World.run.term(term.cont, world, vars)
|
||||
} default {term, world}
|
||||
}
|
||||
log("call!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@call
|
||||
Lit.Core.World.run.term.call(world, vars, term.name, term.func, term.args, term.cont, gas)
|
||||
bind:
|
||||
case world{term.name} as got {
|
||||
none:
|
||||
{term, world}
|
||||
some: case got.value as entry {
|
||||
bond:
|
||||
use func = entry.value
|
||||
let {main, world} = Lit.Core.World.run.term(term.main, world, vars)
|
||||
let world = world{term.name} <- Lit.Core.Entry.bond(func@main <- main)
|
||||
Lit.Core.World.run.term(term.cont, world, vars)
|
||||
} default {term, world}
|
||||
}
|
||||
log("bind!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@bind
|
||||
Lit.Core.World.run.term.bind(world, vars, term.name, term.main, term.cont, gas)
|
||||
}
|
||||
|
||||
Lit.Core.World.run.terms(
|
||||
terms: List<Lit.Core.Term>
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
): Pair<List<Lit.Core.Term>, Lit.Core.World>
|
||||
gas: Nat
|
||||
): Triple<List<Lit.Core.Term>, Lit.Core.World, Nat>
|
||||
case terms {
|
||||
nil:
|
||||
{[], world}
|
||||
{[], world, gas}
|
||||
cons:
|
||||
let {head, world} = Lit.Core.World.run.term(terms.head, world, vars)
|
||||
let {tail, world} = Lit.Core.World.run.terms(terms.tail, world, vars)
|
||||
{head & tail, world}
|
||||
use ctx = Lit.Core.World.run.term(terms.head, world, vars, gas)
|
||||
use tail = Lit.Core.World.run.terms(terms.tail, ctx.world, vars, ctx.gas)
|
||||
{ctx.term & tail.fst, tail.snd, tail.trd}
|
||||
}
|
||||
Lit.Core.World.run.term.call(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
func: String
|
||||
args: List<Lit.Core.Term>
|
||||
cont: Lit.Core.Term
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
case world{func} as got {
|
||||
none:
|
||||
{Lit.Core.Term.call(name, func, args, cont), world, gas}
|
||||
some:
|
||||
case got.value as entry {
|
||||
bond:
|
||||
use func = entry.value
|
||||
let inner_vars = vars
|
||||
let state = Triple.new!!!(inner_vars, world, gas)
|
||||
for arg in List.zip!!(func.input_names, args) with state:
|
||||
// TODO destructuring assignment for triples
|
||||
open state
|
||||
let inner_vars = state.fst
|
||||
let world = state.snd
|
||||
let gas = state.trd
|
||||
let {arg_name, arg_term} = arg
|
||||
use ctx = Lit.Core.World.run.term(arg_term, world, inner_vars, gas)
|
||||
let _ = Lit.Core.run.term.check_sanity(ctx.term) // DEBUG-ish
|
||||
let inner_vars = inner_vars{arg_name} <- ctx.term
|
||||
{inner_vars, ctx.world, ctx.gas}
|
||||
//let {inner_vars, world} = state
|
||||
// TODO destructuring assignment for triples
|
||||
open state
|
||||
let inner_vars = state.fst
|
||||
let world = state.snd
|
||||
let gas = state.trd
|
||||
use ctx = Lit.Core.World.run.term(func.main, world, inner_vars, gas)
|
||||
let _ = Lit.Core.run.term.check_sanity(ctx.term) // DEBUG-ish
|
||||
let vars = vars{name} <- ctx.term
|
||||
Lit.Core.World.run.term(cont, ctx.world, vars, ctx.gas)
|
||||
} default
|
||||
{Lit.Core.Term.call(name, func, args, cont), world, gas}
|
||||
}
|
||||
|
||||
Lit.Core.World.run.term.compare(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
val0: Lit.Core.Term
|
||||
val1: Lit.Core.Term
|
||||
iflt: Lit.Core.Term
|
||||
ifeq: Lit.Core.Term
|
||||
ifgt: Lit.Core.Term
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
use ctx0 = Lit.Core.World.run.term(val0, world, vars, gas)
|
||||
use ctx1 = Lit.Core.World.run.term(val1, ctx0.world, vars, ctx0.gas)
|
||||
case ctx0.term ctx1.term {
|
||||
word word:
|
||||
case U64.cmp(ctx0.term.numb, ctx1.term.numb) {
|
||||
ltn:
|
||||
Lit.Core.World.run.term(iflt, world, vars, ctx1.gas)
|
||||
eql:
|
||||
Lit.Core.World.run.term(ifeq, world, vars, ctx1.gas)
|
||||
gtn:
|
||||
Lit.Core.World.run.term(ifgt, world, vars, ctx1.gas)
|
||||
}
|
||||
} default
|
||||
log("error: operands didn't reduce to words")
|
||||
{Lit.Core.Term.compare(val0, val1, iflt, ifeq, ifgt), world, gas}
|
||||
|
||||
|
||||
Lit.Core.World.run.term.match(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
type: String
|
||||
expr: Lit.Core.Term
|
||||
cses: List<Lit.Core.Term.Case>
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
use ctx = Lit.Core.World.run.term(expr, world, vars, gas)
|
||||
case ctx.term {
|
||||
create: case cses[ctx.term.ctor] as selected_case {
|
||||
some:
|
||||
let {case_fields, case_body} = selected_case.value
|
||||
let substs = List.zip!!(case_fields, ctx.term.vals)
|
||||
let vars = for subst in substs:
|
||||
let {field, value} = subst
|
||||
vars{field} <- value
|
||||
let cost = Lit.Core.Costs.default@match_substitution*List.length!(substs)
|
||||
let gas = ctx.gas + cost
|
||||
Lit.Core.World.run.term(case_body, ctx.world, vars, gas)
|
||||
} default
|
||||
{Lit.Core.Term.match(name, type, ctx.term, cses), world, ctx.gas}
|
||||
} default
|
||||
{Lit.Core.Term.match(name, type, ctx.term, cses), world, ctx.gas}
|
||||
|
||||
Lit.Core.World.run.term.create(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
type: String
|
||||
ctor: Nat
|
||||
vals: List<Lit.Core.Term>
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
use ret = Lit.Core.World.run.terms(vals, world, vars, gas)
|
||||
{Lit.Core.Term.create(type, ctor, ret.fst), ret.snd, ret.trd}
|
||||
|
||||
Lit.Core.World.run.term.var(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
case vars{name} as got {
|
||||
none:
|
||||
{Lit.Core.Term.var(name), world, gas}
|
||||
some:
|
||||
Lit.Core.World.run.term(got.value, world, vars, gas)
|
||||
}
|
||||
|
||||
Lit.Core.World.run.term.operate(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
oper: Lit.Core.Operation
|
||||
val0: Lit.Core.Term
|
||||
val1: Lit.Core.Term
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
use ctx0 = Lit.Core.World.run.term(val0, world, vars, gas)
|
||||
use ctx1 = Lit.Core.World.run.term(val1, ctx0.world, vars, ctx0.gas)
|
||||
case ctx0.term ctx1.term {
|
||||
word word:
|
||||
let numb0 = ctx0.term.numb
|
||||
let numb1 = ctx1.term.numb
|
||||
case oper {
|
||||
add:
|
||||
{Lit.Core.Term.word(numb0 + numb1), world, gas}
|
||||
sub:
|
||||
{Lit.Core.Term.word(numb0 - numb1), world, gas}
|
||||
mul:
|
||||
{Lit.Core.Term.word(numb0 * numb1), world, gas}
|
||||
div:
|
||||
{Lit.Core.Term.word(numb0 / numb1), world, gas}
|
||||
mod:
|
||||
{Lit.Core.Term.word(numb0 % numb1), world, gas}
|
||||
or:
|
||||
{Lit.Core.Term.word(numb0 || numb1), world, gas}
|
||||
and:
|
||||
{Lit.Core.Term.word(numb0 && numb1), world, gas}
|
||||
xor:
|
||||
{Lit.Core.Term.word(U64.xor(numb0, numb1)), world, gas}
|
||||
}
|
||||
} default
|
||||
log("error: operand didn't reduce to word")
|
||||
{Lit.Core.Term.operate(oper, val0, val1), world, gas}
|
||||
|
||||
Lit.Core.World.run.term.bind(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
main: Lit.Core.Term
|
||||
cont: Lit.Core.Term
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
case world{name} as got {
|
||||
none:
|
||||
{Lit.Core.Term.bind(name, main, cont), world, gas}
|
||||
some:
|
||||
case got.value as entry {
|
||||
bond:
|
||||
// TODO calculate gas based upon size of bound term?
|
||||
use func = entry.value
|
||||
use ctx = Lit.Core.World.run.term(main, world, vars, gas)
|
||||
let world = ctx.world{name} <- Lit.Core.Entry.bond(func@main <- ctx.term)
|
||||
Lit.Core.World.run.term(cont, world, vars, ctx.gas)
|
||||
} default
|
||||
{Lit.Core.Term.bind(name, main, cont), world, gas}
|
||||
}
|
||||
|
||||
Lit.Core.run.term.check_sanity(term: Lit.Core.Term): Bool
|
||||
case term {
|
||||
var:
|
||||
log("==> SANITY CHECK FAILED: found term: " | "'" | term.name | "'")
|
||||
false
|
||||
create:
|
||||
let valid = true
|
||||
for val in term.vals with valid:
|
||||
valid && Lit.Core.run.term.check_sanity(val)
|
||||
valid
|
||||
match:
|
||||
let valid = Lit.Core.run.term.check_sanity(term.expr)
|
||||
for cse in term.cses with valid:
|
||||
valid && Lit.Core.run.term.check_sanity(cse@body)
|
||||
valid
|
||||
word:
|
||||
true
|
||||
compare:
|
||||
Lit.Core.run.term.check_sanity(term.val0)
|
||||
&& Lit.Core.run.term.check_sanity(term.val1)
|
||||
&& Lit.Core.run.term.check_sanity(term.iflt)
|
||||
&& Lit.Core.run.term.check_sanity(term.ifeq)
|
||||
&& Lit.Core.run.term.check_sanity(term.ifgt)
|
||||
operate:
|
||||
Lit.Core.run.term.check_sanity(term.val0)
|
||||
&& Lit.Core.run.term.check_sanity(term.val1)
|
||||
call:
|
||||
// TODO I don't know what I'm doing
|
||||
// should this return false (invalid) ?
|
||||
let valid = true
|
||||
for arg in term.args with valid:
|
||||
valid && Lit.Core.run.term.check_sanity(arg)
|
||||
valid && Lit.Core.run.term.check_sanity(term.cont)
|
||||
bind:
|
||||
Lit.Core.run.term.check_sanity(term.main)
|
||||
&& Lit.Core.run.term.check_sanity(term.cont)
|
||||
}
|
||||
|
||||
|
||||
//
|
||||
// Tests
|
||||
// -----
|
||||
|
||||
Lit.Core: _
|
||||
let world = {}
|
||||
|
||||
@ -681,64 +795,70 @@ Lit.Core: _
|
||||
| Lit.Lang.Bits
|
||||
| Lit.Lang.BitsMap
|
||||
| Lit.Lang.Voting
|
||||
// | Lit.Lang.Test
|
||||
//| Lit.Lang.Test
|
||||
|
||||
// let code = code |
|
||||
// `
|
||||
// GiveUnit(): Unit
|
||||
// Unit/new
|
||||
// let code = code |
|
||||
// `
|
||||
// GiveUnit(): Unit
|
||||
// Unit/new
|
||||
//
|
||||
// TakeUnit(x: Unit): U64
|
||||
// 42
|
||||
//
|
||||
// do {
|
||||
// call a1 = GiveUnit()
|
||||
// call a2 = GiveUnit()
|
||||
// call b = TakeUnit(a1)
|
||||
// call c = TakeUnit(a2)
|
||||
// (+ b c)
|
||||
// }
|
||||
// `
|
||||
|
||||
// TakeUnit(x: Unit): U64
|
||||
// 42
|
||||
|
||||
// do {
|
||||
// call a1 = GiveUnit()
|
||||
// call a2 = GiveUnit()
|
||||
// call b = TakeUnit(a1)
|
||||
// call c = TakeUnit(a2)
|
||||
// (+ b c)
|
||||
// }
|
||||
// `
|
||||
|
||||
// let code = code |
|
||||
// `
|
||||
// //type Lit.Core.Operation {
|
||||
// // add ok!
|
||||
// // sub ok!
|
||||
// // mul ok!
|
||||
// // div ok!
|
||||
// // mod ok!
|
||||
// // or ok!
|
||||
// // and ok!
|
||||
// // xor ok!
|
||||
// //}
|
||||
// WordTest(): U64
|
||||
// cmp 2 3 {
|
||||
// ltn:
|
||||
// 0
|
||||
// eql:
|
||||
// 1
|
||||
// gtn:
|
||||
// 2
|
||||
// }
|
||||
// do {
|
||||
// call b = WordTest()
|
||||
// b
|
||||
// }
|
||||
// `
|
||||
let code = code |
|
||||
`
|
||||
// type Lit.Core.Costs {
|
||||
// new(
|
||||
// var: Nat
|
||||
// create: Nat
|
||||
// match: Nat
|
||||
// match_substitution: Nat
|
||||
// word: Nat
|
||||
// compare: Nat
|
||||
// operate: Nat
|
||||
// call: Nat
|
||||
// bind: Nat
|
||||
// )
|
||||
// }
|
||||
// WordTest(): U64
|
||||
// cmp 2 3 {
|
||||
// ltn:
|
||||
// 0
|
||||
// eql:
|
||||
// 1
|
||||
// gtn:
|
||||
// 2
|
||||
// }
|
||||
TestWord(): U64
|
||||
0
|
||||
do {
|
||||
bind TestWord = 1
|
||||
0
|
||||
}
|
||||
`
|
||||
|
||||
let page = Parser.run!(Lit.Lang.parser.page(world), code) abort IO.print("parse error")
|
||||
log("parsed:")
|
||||
log(Lit.Lang.show.page(page, world))
|
||||
|
||||
log("PARSED:") // DEBUG
|
||||
log(Lit.Lang.show.page(page, world)) // DEBUG
|
||||
|
||||
case Lit.Core.World.run.page(page, world) as result {
|
||||
none:
|
||||
IO.print("FAILURE")
|
||||
some:
|
||||
IO {
|
||||
// log("page:")
|
||||
// let new_world = result.value
|
||||
// log(Lit.Lang.show.page(page, new_world))
|
||||
// log("PAGE:") // DEBUG
|
||||
// let new_world = result.value // DEBUG
|
||||
// log(Lit.Lang.show.page(page, new_world)) // DEBUG
|
||||
IO.print("SUCCESS")
|
||||
}
|
||||
}
|
||||
|
@ -5,9 +5,9 @@ In 2013, the first smart-contract blockchain, Ethereum, was proposed, extending
|
||||
Bitcoin with a stateful scripting language that allowed arbitrary financial
|
||||
transactions to be settled without third parties. Notably, Ethereum's built-in
|
||||
virtual machine made it a general-purpose computer, even though most of the
|
||||
protocol's complexity wasn't required to achieve Turing completeness. Litereum
|
||||
protocol's complexity was not required to achieve Turing completeness. Litereum
|
||||
is a massive simplification of this concept, trading features for raw
|
||||
simplicity. Since it doesn't have a native token, it isn't a cryptocurrency
|
||||
simplicity. Since it does not have a native token, it is not a cryptocurrency
|
||||
itself, but currencies can be created as internal programs. In essence, Litereum
|
||||
is a peer-to-peer Lambda Calculus interpreter, making it a minimal decentralized
|
||||
computer, and a politically neutral smart-contract platform.
|
||||
@ -31,7 +31,7 @@ Having a simpler implementation has two major benefits.
|
||||
Since there is less code, the attack surface is narrower, making a full node
|
||||
much easier to audit. Moreover, the internal scripting language is prone to
|
||||
formal verification, further reinforcing security. This is only possible because
|
||||
it isn't based on stack machines, but on a simply-typed affine calculus that is
|
||||
it is not based on stack machines, but on a simply-typed affine calculus that is
|
||||
type-checked on-chain and has a clear cost model, preventing reentrancy attacks
|
||||
(that would lead to invalid states, hindering formal verification) and spam
|
||||
(which would be unavoidable in the usual lambda calculus, due to the
|
||||
@ -56,12 +56,12 @@ Below are some of the major differences that make this possible:
|
||||
|
||||
Ethereum uses the Elliptic Curve Digital Signature Algorithm (ECDSA) for message
|
||||
authentication as a hard-coded algorithm that is part of the protocol. As of
|
||||
2021, it is still not possible to create Ethereum accounts that don't depend on
|
||||
2021, it is still not possible to create Ethereum accounts that do not depend on
|
||||
ECDSA signatures. Since ECDSA is vulnerable to quantum attackers, if a quantum
|
||||
computer of reasonable scale is developed, most Ethereum accounts will have
|
||||
their private keys exposed, which would be catastrophic to the network.
|
||||
|
||||
Litereum doesn't have a native account system or signature scheme. Instead,
|
||||
Litereum does not have a native account system or signature scheme. Instead,
|
||||
users create accounts by simply deploying smart-contracts that they control
|
||||
through their preferred authentication scheme. As such, users are free to use a
|
||||
cheaper, but less secure, signature algorithm, like ECDSA, or an expensive, but
|
||||
@ -75,7 +75,7 @@ not only has no "preferred currency", but it has no built-in currency at all: it
|
||||
is a pure computation network. Of course, users can still create their own
|
||||
tokens as contracts, but every internal currency is treated equally.
|
||||
|
||||
As a consequence, Litereum transactions don't have the "from", "to", "value",
|
||||
As a consequence, Litereum transactions do not have the "from", "to", "value",
|
||||
"gasPrice" or "gasLimit" fields. Instead, a transaction is just a block of code
|
||||
that is executed when mined in order to alter the blockchain state.
|
||||
Ethereum-like transactions can be emulated by a suitable script. For example,
|
||||
@ -97,10 +97,10 @@ same behavior as a classic Ethereum transaction.
|
||||
Like Ethereum, the computational cost of a transaction is measured in gas, and
|
||||
blocks have a size (space) and gas (time) limit. This keeps the cost of running
|
||||
a full node, both in terms of computation and storage cost, predictable. Since
|
||||
there isn't a native currency, there isn't a built-in gas-to-native-token
|
||||
there is not a native currency, there is not a built-in gas-to-native-token
|
||||
conversion either. Instead, a free market emerges, where users choose the exact
|
||||
amount of fees they want to pay, and miners select transactions that fit in a
|
||||
block, considering both space and computation costs, in a manner that maximies
|
||||
block, considering both space and computation costs, in a manner that maximizes
|
||||
their individual profits.
|
||||
|
||||
#### 3. A simpler block structure
|
||||
@ -115,7 +115,7 @@ patricia-merkle trees).
|
||||
Litereum takes a minimalistic approach: blocks store just the previous block,
|
||||
the nonce, the miner identity and a list of transactions (which are, themselves,
|
||||
just blocks of code). Of course, that means that features like light clients
|
||||
aren't possible, but we argue that these aren't used in practice: users either
|
||||
are not possible, but we argue that these are not used in practice: users either
|
||||
run full nodes, or trust someone that does.
|
||||
|
||||
#### 4. A simple concensus algorithm
|
||||
@ -134,20 +134,20 @@ Litereum's code.
|
||||
#### 5. It is slower
|
||||
|
||||
Finally, it must be stressed that Litereum is not designed to have a high layer
|
||||
1 throughput. It has a very limited block size and computation budget. This
|
||||
allows us to avoid design choices that would make it more scalable for the cost
|
||||
of added complexity. In general, Litereum should be less scalable than Ethereum
|
||||
on its layer 1.
|
||||
1 throughput. It has a very limited block size and computation budget. Thus, its
|
||||
complexity is reduced, but at the cost of being less scalable than Ethereum on
|
||||
its layer 1.
|
||||
|
||||
There are, though, key differences that make it better in some cases. For
|
||||
example, deploying contracts don't require signatures, and these are smaller
|
||||
than their Ethereum counterparts, due to shorter serialization and global
|
||||
sharing of functions. Deploying blocks and performing non-signed calls should be
|
||||
more scalable on Litereum.
|
||||
However, there are key differences that are a better fit for some scenarios.
|
||||
For example, the deployment of contracts does not require signatures; These
|
||||
contracts are smaller than their Ethereum counterparts for technical aspects
|
||||
such as shorter serialization and global sharing of functions. Therefore,
|
||||
deploying blocks and performing non-signed calls should be more scalable on
|
||||
Litereum.
|
||||
|
||||
Regardless, we argue that layer 1 scalability is not the most important
|
||||
end-goal. Most layer 2 optimizations that make Ethereum more scalable apply to
|
||||
Litereum, so, a slower layer 1 won't detain long-term scalability.
|
||||
Litereum, so, a slower layer 1 will not detain long-term scalability.
|
||||
|
||||
Design
|
||||
------
|
||||
@ -249,7 +249,7 @@ A function has 6 fields:
|
||||
|
||||
A top-level command that alters the global state. Commands are grouped in pages.
|
||||
Tracing a parallel to conventional blockchains, a command is like a transaction,
|
||||
and a page is like a block. The main difference is that commands don't need to
|
||||
and a page is like a block. The main difference is that commands do not need to
|
||||
be signed. There are 4 variants of commands:
|
||||
|
||||
##### 1. `new_type(type)`
|
||||
@ -266,11 +266,11 @@ If the function's name already exists, then this command fails.
|
||||
|
||||
If the function's body is ill-typed with a type context initialized with the
|
||||
function's argument list, then this command fails. The function body
|
||||
is ill-typed if it doesn't pass the type-check procedure, with a type context
|
||||
is ill-typed if it does not pass the type-check procedure, with a type context
|
||||
initialized with each variable on the function's argument list.
|
||||
|
||||
If the function's body is invalid, then this command fails. The function body is
|
||||
invalid if it doesn't pass the validate procecure.
|
||||
invalid if it does not pass the validate procedure.
|
||||
|
||||
##### 3. `new_user(user)`
|
||||
|
||||
@ -286,10 +286,10 @@ If the signature is invalid, the command is executed anonymously, with the
|
||||
username being set as the empty bitstring.
|
||||
|
||||
If the expression's body is ill-typed, then this command fails. The function body
|
||||
is ill-typed if it doesn't pass the type-check procedure with an empty context.
|
||||
is ill-typed if it does not pass the type-check procedure with an empty context.
|
||||
|
||||
If the expression's body is invalid, then this command fails. The expression
|
||||
body is invalid if it doesn't pass the validate procedure.
|
||||
body is invalid if it does not pass the validate procedure.
|
||||
|
||||
#### Term
|
||||
|
||||
@ -302,7 +302,7 @@ Represents a variable bound by a global function, or by a pattern-matching
|
||||
clause. When a function is called, or a pattern-match takes place, the bound
|
||||
variable will be substituted by its called, or matched, value. Variables must be
|
||||
affine, which means the same bound variable can only be used at most once, and
|
||||
must be unique, which means the same name can't be bound to two different
|
||||
must be unique, which means the same name cannot be bound to two different
|
||||
variables, globally.
|
||||
|
||||
##### 2. `create(type, form, vals)`
|
||||
@ -325,7 +325,7 @@ A create variant is well-typed if:
|
||||
its type matches the type stored on `fields[i]`, where `fields` is the list
|
||||
of fields stored on the constructor of number `ctor` in the selected type
|
||||
|
||||
The create variant doesn't compute. It is irreducible.
|
||||
The create variant does not compute. It is irreducible.
|
||||
|
||||
##### 3. `match`
|
||||
|
||||
@ -410,11 +410,11 @@ type Lit.Cons.Page {
|
||||
}
|
||||
```
|
||||
|
||||
Unlike Bitcoin blocks, a LitCons page doesn't hold a set of transactions.
|
||||
Unlike Bitcoin blocks, a LitCons page does not hold a set of transactions.
|
||||
Instead, it stores an arbitrary blob of 1280 bytes of data. The size was chosen
|
||||
to allow a full block to fit in a small UDP packet, allowing for fast
|
||||
propagation. There are no "block headers": a page stores all its data. There
|
||||
aren't native tokens, nor transaction fees. The incentives to include Litereum
|
||||
are not native tokens, nor transaction fees. The incentives to include Litereum
|
||||
commands (transactions) in a page are determined by miners and users: fees can
|
||||
be paid with any internal token.
|
||||
|
||||
|
@ -1,5 +1,10 @@
|
||||
Test: _
|
||||
Lit.Core
|
||||
case 2 as two {
|
||||
zero:
|
||||
?a
|
||||
succ:
|
||||
?b
|
||||
}
|
||||
|
||||
//Test: String
|
||||
//let idx = 0
|
||||
|
7
base/Triple.kind
Normal file
7
base/Triple.kind
Normal file
@ -0,0 +1,7 @@
|
||||
type Triple <A: Type, B: Type, C: Type> {
|
||||
new(
|
||||
fst: A
|
||||
snd: B
|
||||
trd: C
|
||||
)
|
||||
}
|
Loading…
Reference in New Issue
Block a user