HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-09-11 08:45:32 +03:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #306 from kind-lang/RLP_fix

Browse Source 
RLP proof
This commit is contained in:
Rígille S. B. Menezes 2021-12-03 15:12:12 -03:00 committed by GitHub
commit bd53786d77
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
99 changed files with 1404 additions and 1188 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
base/Bool/and/split.kind Normal file
View File

@ -0,0 +1,12 @@
Bool.and.split(a: Bool, b: Bool): Bool.and(a, b)(() Type, And<a == true, b == true>, Or<a == false, b == false>)
case a {
true:
case b {
true:
{refl, refl}
false:
right(refl)
}!
false:
left(refl)
}!

7
base/Bool/xor.kind Normal file
View File

@ -0,0 +1,7 @@
Bool.xor(a: Bool, b: Bool): Bool
case a {
true:
Bool.not(b)
false:
b
}

79
base/Bytes.kind
View File

@ -1,49 +1,44 @@
// Bytes
// =====
//Byte: Type
//Word<8>
Bytes: Type
List<U8>
Bytes.show(bytes: Bytes): String
List.show!(Bits.show, List.map!!(U8.to_bits, bytes))
Bytes.to_nat.go<size: Nat>(byte: Word<size>): Nat
case byte {
e: Nat.zero
o: Nat.double(Bytes.to_nat.go<byte.size>(byte.pred))
i: Nat.succ(Nat.double(Bytes.to_nat.go<byte.size>(byte.pred)))
}
Bytes.split: (bytes: Bytes, n: Nat) -> Pair<Bytes, Bytes>
List.split<U8>
Bytes.to_nat(bytes: Bytes): Nat
Bytes.to_nat.go(bytes, 0)
Bytes.to_nat.go(bytes: Bytes, acc: Nat): Nat
case bytes {
nil:
Nat.zero
cons:
let head = Bytes.to_nat.go<8>(bytes.head@value)
let tail = Bytes.to_nat(bytes.tail)
Nat.add(head, Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(tail)))))))))
}
Bytes.from_nat.go(n: Nat, r: Bytes): Bytes
case n {
zero: r
succ: Bytes.from_nat.go(n.pred, Bytes.inc(r))
acc
cons:
let digit = U8.to_nat(bytes.head)
Bytes.to_nat.go(bytes.tail, (acc*256) + digit)
}
Bytes.from_nat(n: Nat): Bytes
Bytes.from_nat.go(n, [])
case n {
zero:
List.nil!
succ:
Bytes.from_nat(n/256) ++ [U8.from_nat(Nat.mod(n, 256))]
}
//Bytes.inc.go<size: Nat>(byte: Word<size>): Pair<Word<size>, Bool>
//case byte {
//e: {Word.e, true}
//o: {Word.i!(byte.pred), false}
//i: case Bytes.inc.go!(byte.pred) as result {
//new: {Word.o!(result.fst), result.snd}
//}
//}!
Bytes.to_hex(b: Bytes): String
Bytes.to_hex.go("", b)
Bytes.to_hex.go(acc: String, b: Bytes): String
case b {
nil:
acc
cons:
Bytes.to_hex.go(acc|U8.to_hex(b.head), b.tail)
}
Bytes.inc(bytes: Bytes): Bytes
case bytes {
@ -55,27 +50,3 @@ Bytes.inc(bytes: Bytes): Bytes
else
List.cons!(U8.inc(bytes.head), bytes.tail)
}
//case bytes {
//nil: [1#8]
//cons: case Bytes.inc.go!(bytes.head@value) as result {
//new: case result.snd {
//true: List.cons!(U8.new(result.fst), Bytes.inc(bytes.tail))
//false: List.cons!(U8.new(result.fst), bytes.tail)
//}
//}
//}
//Bytes.from_nat.identity(n: Nat): Equal<Nat, Bytes.to_nat(Bytes.from_nat(n)), n>
//Bytes.from_nat.identity(n)
//Aux.1(
//n: Nat
//e0: Nat.ltn(0, n) == true
//e1: Nat.ltn(n, 256) == true
//): Equal<Bytes, Bytes.from_nat(n), [Nat.apply!(n, Word.inc<8>, Word.zero(8))]>
//Aux.1(n, e0, e1)

70
base/Bytes/to_nat/concat.kind Normal file
View File

@ -0,0 +1,70 @@
Bytes.to_nat.concat(
b0: Bytes, b1: Bytes
): (Bytes.to_nat(b1) + Nat.pow(256, List.length(U8, b1))*Bytes.to_nat(b0)) == Bytes.to_nat(b0 ++ b1)
case b1 {
nil:
case List.concat.nil_right(U8, b0) {
refl:
Nat.add.zero_right(Bytes.to_nat(b0))
}: Nat.add(Bytes.to_nat(List.nil(U8)),Nat.mul(Nat.pow(256,List.length(U8,List.nil(U8))),Bytes.to_nat(b0))) == Bytes.to_nat(self.b)
cons:
let reassoc = mirror(List.concat.assoc(U8, b0, [b1.head], b1.tail))
case reassoc {
refl:
let ind = Bytes.to_nat.concat(List.concat(U8,b0,[b1.head]),b1.tail)
case ind {
// proof sketch:
// to_nat(bh & bt) + 256^succ(len(bt)) * to_nat(t) == to_nat(bt) + 256^len(bt) * to_nat(t ++ [bh])
// (to_nat(bt) + 256^len(bt)*to_nat([bh])) + 256^succ(len(bt)) * to_nat(t) == to_nat(bt) + 256^len(bt) * to_nat(t ++ [bh])
// to_nat(bt) + (256^len(bt)*to_nat([bh]) + 256^succ(len(bt)) * to_nat(t)) == to_nat(bt) + 256^len(bt) * to_nat(t ++ [bh])
// (256^len(bt)*to_nat([bh]) + 256^succ(len(bt)) * to_nat(t)) == 256^len(bt) * to_nat(t ++ [bh])
// (256^len(bt)*to_nat([bh]) + (256*256^len(bt)) * to_nat(t)) == 256^len(bt) * to_nat(t ++ [bh])
// (256^len(bt)*to_nat([bh]) + (256^len(bt)*256) * to_nat(t)) == 256^len(bt) * to_nat(t ++ [bh])
// (256^len(bt)*to_nat([bh]) + 256^len(bt)*(256 * to_nat(t)) == 256^len(bt) * to_nat(t ++ [bh])
// 256^len(bt)*(to_nat([bh] + 255*to_nat(t))) == 256^len(bt) * to_nat(t ++ [bh])
// 256^len(bt)*(to_nat([bh] + 255*to_nat(t))) == 256^len(bt) * (to_nat([bh]) + 256*to_nat(t))
refl:
let ind = Bytes.to_nat.concat([b1.head], b1.tail)
case ind {
refl:
let reassoc = mirror(Nat.add.assoc(Bytes.to_nat(b1.tail), Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Bytes.to_nat(List.cons(U8,b1.head,List.nil(U8)))), Nat.mul(Nat.pow(256,List.length(U8,List.cons(U8,b1.head,b1.tail))),Bytes.to_nat(b0))))
case reassoc {
refl:
let mul_reassoc = case mirror(Nat.mul.assoc(Nat.pow(256,List.length(U8,b1.tail)),256, Bytes.to_nat(b0))) {
refl:
case Nat.mul.comm(256, Nat.pow(256,List.length(U8,b1.tail))) {
refl:
Equal.refl(Nat, Nat.mul(Nat.mul(256,Nat.pow(256,List.length(U8,b1.tail))),Bytes.to_nat(b0)))
}: Nat.mul( self.b, Bytes.to_nat(b0)) == Nat.mul(Nat.pow(256,List.length(U8,List.cons(U8,b1.head,b1.tail))),Bytes.to_nat(b0))
}: self.b == Nat.mul(Nat.pow(256,List.length(U8,List.cons(U8,b1.head,b1.tail))),Bytes.to_nat(b0))
let lemma = case mul_reassoc {
refl:
let mul_factor = Nat.mul.distrib_left(Nat.pow(256,List.length(U8,b1.tail)), Bytes.to_nat(List.cons(U8,b1.head,List.nil(U8))), Nat.mul(256,Bytes.to_nat(b0)))
case mul_factor {
refl:
let ind = Bytes.to_nat.concat(b0, List.cons(U8, b1.head, List.nil(U8)))
case ind {
refl:
let obvious = mirror(Nat.mul.one_right(256)) :: Equal(Nat, 256, Nat.pow(256,List.length(U8,List.cons(U8,b1.head,List.nil(U8)))))
case obvious {
refl:
refl
}: Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Nat.add(Bytes.to_nat(List.cons(U8,b1.head,List.nil(U8))),Nat.mul(256,Bytes.to_nat(b0)))) == Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Nat.add(Bytes.to_nat(List.cons(U8,b1.head,List.nil(U8))),Nat.mul( obvious.b, Bytes.to_nat(b0))))
}: Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Nat.add(Bytes.to_nat(List.cons(U8,b1.head,List.nil(U8))),Nat.mul(256,Bytes.to_nat(b0)))) == Nat.mul(Nat.pow(256,List.length(U8,b1.tail)), ind.b )
}: mul_factor.b == Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Bytes.to_nat(List.concat(U8,b0,List.cons(U8,b1.head,List.nil(U8)))))
}: Nat.add(Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Bytes.to_nat(List.cons(U8,b1.head,List.nil(U8)))), mul_reassoc.b ) == Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Bytes.to_nat(List.concat(U8,b0,List.cons(U8,b1.head,List.nil(U8)))))
case lemma {
refl:
refl
}: Nat.add(Bytes.to_nat(b1.tail),Nat.add(Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Bytes.to_nat(List.cons(U8,b1.head,List.nil(U8)))),Nat.mul(Nat.pow(256,List.length(U8,List.cons(U8,b1.head,b1.tail))),Bytes.to_nat(b0)))) == Nat.add(Bytes.to_nat(b1.tail), lemma.b )
}: reassoc.b == Nat.add(Bytes.to_nat(b1.tail),Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Bytes.to_nat(List.concat(U8,b0,List.cons(U8,b1.head,List.nil(U8))))))
}: Nat.add(ind.b, Nat.mul(Nat.pow(256,List.length(U8,List.cons(U8,b1.head,b1.tail))),Bytes.to_nat(b0))) == Nat.add(Bytes.to_nat(b1.tail),Nat.mul(Nat.pow(256,List.length(U8,b1.tail)),Bytes.to_nat(List.concat(U8,b0,List.cons(U8,b1.head,List.nil(U8))))))
}: Nat.add(Bytes.to_nat(List.cons(U8,b1.head,b1.tail)),Nat.mul(Nat.pow(256,List.length(U8,List.cons(U8,b1.head,b1.tail))),Bytes.to_nat(b0))) == ind.b
}: Nat.add(Bytes.to_nat(List.cons(U8,b1.head,b1.tail)),Nat.mul(Nat.pow(256,List.length(U8,List.cons(U8,b1.head,b1.tail))),Bytes.to_nat(b0))) == Bytes.to_nat(reassoc.b)
}!

37
base/Bytes/to_nat/from_nat.kind Normal file
View File

@ -0,0 +1,37 @@
Bytes.to_nat.from_nat(n: Nat): n == Bytes.to_nat(Bytes.from_nat(n))
case n {
zero:
refl
succ:
let ind = Bytes.to_nat.concat(Bytes.from_nat(Nat.div(Nat.succ(n.pred),256)),List.cons(U8,U8.from_nat(Nat.mod(Nat.succ(n.pred),256)),List.nil(U8)))
case ind {
refl:
let mod_small = Nat.lte.comm.false(256, Nat.mod(Nat.succ(n.pred), 256), Nat.mod.small(Nat.succ(n.pred), 256, refl))
let mod_safe_conversion = Nat.to_u8.safe_conversion(Nat.mod(Nat.succ(n.pred),256), mod_small)
case mod_safe_conversion {
refl:
let len_one = refl :: Equal(Nat, 1, List.length(U8,List.cons(U8,U8.from_nat(Nat.mod(Nat.succ(n.pred),256)),List.nil(U8))))
let pow_one = case len_one {
refl:
Nat.pow.one_right(256)
}: Equal(Nat, 256, Nat.pow(256, len_one.b))
case pow_one {
refl:
let ind = Bytes.to_nat.from_nat(Nat.div(Nat.succ(n.pred),256))
case ind {
refl:
let comm = Nat.mul.comm(Nat.div(Nat.succ(n.pred),256), 256)
case comm {
refl:
mirror(Nat.div_mod.recover(Nat.succ(n.pred), 256, refl))
}: Equal(Nat, Nat.succ(n.pred), Nat.add(Nat.mod(Nat.succ(n.pred),256),comm.b))
}: Equal(Nat, Nat.succ(n.pred), Nat.add(Nat.mod(Nat.succ(n.pred),256),Nat.mul(256,ind.b)))
}: Equal(Nat, Nat.succ(n.pred), Nat.add(Nat.mod(Nat.succ(n.pred),256),Nat.mul( pow_one.b, Bytes.to_nat(Bytes.from_nat(Nat.div(Nat.succ(n.pred),256))))))
}: Equal(Nat, Nat.succ(n.pred), Nat.add( mod_safe_conversion.b, Nat.mul(Nat.pow(256,List.length(U8,List.cons(U8,U8.from_nat(Nat.mod(Nat.succ(n.pred),256)),List.nil(U8)))),Bytes.to_nat(Bytes.from_nat(Nat.div(Nat.succ(n.pred),256))))))
}: Equal(Nat, Nat.succ(n.pred), ind.b)
}!

40
base/Equal/vapply.kind Normal file
View File

@ -0,0 +1,40 @@
Equal.vapply(
n: Nat
X: Type
): Equal.vapply.type(n, X, X, (x) x, (x) x)
Equal.vapply.aux(n, X, X, (x) x, (x) x, (f) refl)
Equal.vapply.type(
n: Nat
X: Type
ftype: Type
acc_left: ftype -> X
acc_right: ftype -> X
): Type
case n {
zero:
(f: ftype) -> Equal<X>(acc_left(f), acc_right(f))
succ:
<A: Type> -> (a0: A, a1: A, ae: Equal<A>(a0, a1)) ->
Equal.vapply.type(n.pred, X, A -> ftype, (f) acc_left(f(a0)), (f) acc_right(f(a1)))
}
Equal.vapply.aux(
n: Nat
X: Type
ftype: Type
acc_left: ftype -> X
acc_right: ftype -> X
Hyp: (f: ftype) -> Equal<X>(acc_left(f), acc_right(f))
): Equal.vapply.type(n, X, ftype, acc_left, acc_right)
case n {
zero:
Hyp
succ:
(A, a0, a1, ae)
let lemma = (f)
let both_a0 = Hyp(f(a0))
let qed = both_a0 :: rewrite R in Equal<X>(acc_left(f(a0)), acc_right(f(R))) with ae
qed
Equal.vapply.aux(n.pred, X, A -> ftype, (f) acc_left(f(a0)), (f) acc_right(f(a1)), lemma)
}!

28
base/Ether/RLP.kind Normal file
View File

@ -0,0 +1,28 @@
// The RLP format
//
// Serialization and deserialization for the BytesTree type, under the following grammar:
// | First byte | Meaning |
// | ---------- | -------------------------------------------------------------------------- |
// | 0 to 127 | HEX(leaf) |
// | 128 to 183 | HEX(length_of_leaf + 128) + HEX(leaf) |
// | 184 to 191 | HEX(length_of_length_of_leaf + 128 + 56) + HEX(length_of_leaf) + HEX(leaf) |
// | 192 to 247 | HEX(length_of_node + 192) + HEX(node) |
// | 248 to 255 | HEX(length_of_length_of_node + 192 + 56) + HEX(length_of_node) + HEX(node) |
//
// The first byte of Ether.RLP.encode.length
// buffer length (len) | Ether.RLP.encode.length(add,len)[0]
// ------------------- | -----------------------------
// 56 ~ 256**1-1 | 185
// 256**1 ~ 256**2-1 | 186
// 256**2 ~ 256**3-1 | 187
// 256**3 ~ 256**4-1 | 188
// 256**4 ~ 256**5-1 | 189
// 256**5 ~ 256**6-1 | 190
// 256**6 ~ 256**7-1 | 191
// Type
// ----
type Ether.RLP {
data(value: List<U8>)
node(child: List<Ether.RLP>)
}

2
base/Ether/RLP/Constants/bits_128.kind
View File

@ -1,2 +0,0 @@
Ether.RLP.Constants.bits_128 : Bits
Nat.to_bits(128)

2
base/Ether/RLP/Constants/bits_184.kind
View File

@ -1,2 +0,0 @@
Ether.RLP.Constants.bits_184 : Bits
Nat.to_bits(184)

2
base/Ether/RLP/Constants/bits_192.kind
View File

@ -1,2 +0,0 @@
Ether.RLP.Constants.bits_192 : Bits
Nat.to_bits(192)

2
base/Ether/RLP/Constants/bits_248.kind
View File

@ -1,2 +0,0 @@
Ether.RLP.Constants.bits_248 : Bits
Nat.to_bits(248)

2
base/Ether/RLP/Constants/bits_255.kind
View File

@ -1,2 +0,0 @@
Ether.RLP.Constants.bits_255 : Bits
Nat.to_bits(255)

3
base/Ether/RLP/README.md
View File

@ -1,5 +1,4 @@
# RLP
The purpose of RLP (Recursive Length Prefix) is to encode arbitrarily nested arrays of binary data, and RLP is the main encoding method used to serialize objects in Ethereum. The only purpose of RLP is to encode structure; encoding specific data types (eg. strings, floats) is left up to higher-order protocols;
### Example
@ -17,4 +16,4 @@ The string “Lorem ipsum dolor sit amet, consectetur adipisicing elit” = `[ 0
### Reference
- [Ethereum Wiki](https://eth.wiki/fundamentals/rlp)
- [Ethers.js](https://github.com/ethers-io/ethers.js/tree/master/packages/rlp)
- [Ethers.js](https://github.com/ethers-io/ethers.js/tree/master/packages/rlp)

5
base/Ether/RLP/Tree.kind
View File

@ -1,5 +0,0 @@
//changed to become a functor
type Ether.RLP.Tree<A : Type> {
tip(value : A)
list(value : List<Ether.RLP.Tree<A>>)
}

93
base/Ether/RLP/aux.kind Normal file
View File

@ -0,0 +1,93 @@
// These are lemmas about how RLP decoding may split a list of Bytes
Ether.RLP.aux.split.0(
payload: Bytes
tail: Bytes
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
): Pair.new(Bytes, Bytes, payload, tail) == Ether.RLP.split.length(128, Nat.to_u8(Nat.add(128, List.length!(payload))) & payload ++ tail)
let chain = Nat.Order.chain(List.length(U8,payload), 55, 126, H, refl)
let H0 = Nat.ltn.sub_right(128, List.length(U8,payload), 255, chain)
let H1 = Nat.to_u8.safe_conversion(Nat.add(128,List.length(U8,payload)), H0)
replace X with H1 in Pair.new(Bytes,Bytes,payload,tail) == Nat.lte(Nat.sub(X,128),55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,payload,tail),Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128)),Bytes.split(List.concat(U8,payload,tail),Nat.sub(Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
let H2 = Nat.sub.add.left(128, List.length(U8,payload)) :: rewrite X in Nat.sub(X,128) == List.length(U8,payload) with Nat.add.comm(List.length(U8,payload),128)
replace X with mirror(H2) in Pair.new(Bytes,Bytes,payload,tail) == Nat.lte(X,55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,payload,tail),Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128)),Bytes.split(List.concat(U8,payload,tail),Nat.sub(Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
replace X with mirror(H) in Pair.new(Bytes,Bytes,payload,tail) == X(() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,payload,tail),Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128)),Bytes.split(List.concat(U8,payload,tail),Nat.sub(Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
replace X with H1 in Pair.new(Bytes,Bytes,payload,tail) == Bytes.split(List.concat(U8,payload,tail),Nat.sub(X,128))
replace X with mirror(H2) in Pair.new(Bytes,Bytes,payload,tail) == Bytes.split(List.concat(U8,payload,tail),X)
let split = List.split.length!(payload, tail)
mirror(split)
Ether.RLP.aux.split.1(
payload: Bytes
tail: Bytes
H0: Equal<Bool>(Nat.lte(List.length!(payload), 55), false)
H1: Equal<Bool>(Nat.lte(List.length(U8, payload), Ether.RLP.max), true)
): Pair.new(Bytes, Bytes, payload, tail) ==
let b = Bytes.from_nat(List.length!(payload))
let a = Nat.to_u8(Nat.add(56, Nat.add(128, List.length!(b))))
Ether.RLP.split.length(128, a & (b ++ payload) ++ tail)
let bytes_from_nat_length = Nat.lte.slack_left(List.length(U8, Bytes.from_nat(List.length(U8,payload))), 7, 64, Ether.RLP.aux.bytes_from_nat(List.length(U8, payload), H1))
let safe_conversion = Nat.to_u8.safe_conversion(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,payload))))), bytes_from_nat_length)
case safe_conversion {
refl:
let concat_assoc = List.concat.assoc(U8,Bytes.from_nat(List.length(U8,payload)),payload,tail)
case concat_assoc {
refl:
let splitted_pair = mirror(List.split.length(U8, Bytes.from_nat(List.length(U8,payload)), List.concat(U8, payload, tail)))
case splitted_pair {
refl:
let recover_length = Bytes.to_nat.from_nat(List.length(U8,payload))
case recover_length {
refl:
mirror(List.split.length(U8, payload, tail))
}: Pair.new(Bytes,Bytes,payload,tail) == List.split(U8, List.concat(U8, payload, tail), recover_length.b)
}: Pair.new(Bytes,Bytes,payload,tail) == splitted_pair.b( () Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length)))
}: Pair.new(Bytes,Bytes,payload,tail) == Bytes.split( concat_assoc.b, Nat.sub(Nat.sub(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,payload))))),128),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length)))
}: Pair.new(Bytes,Bytes,payload,tail) == Nat.lte(Nat.sub( safe_conversion.b, 128),55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,payload)),payload),tail),Nat.sub( safe_conversion.b, 128)),Bytes.split(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,payload)),payload),tail),Nat.sub(Nat.sub( safe_conversion.b, 128),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
Ether.RLP.aux.split.2(
payload: Bytes
tail: Bytes
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
): Pair.new(Bytes, Bytes, payload, tail) == Ether.RLP.split.length(192, Nat.to_u8(Nat.add(192, List.length!(payload))) & payload ++ tail)
let chain = Nat.Order.chain(List.length(U8,payload), 55, 62, H, refl)
let H0 = Nat.ltn.sub_right(192, List.length(U8,payload), 255, chain)
let H1 = Nat.to_u8.safe_conversion(Nat.add(192,List.length(U8,payload)), H0)
replace X with H1 in Pair.new(Bytes,Bytes,payload,tail) == Nat.lte(Nat.sub(X,192),55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,payload,tail),Nat.sub(X,192)),Bytes.split(List.concat(U8,payload,tail),Nat.sub(Nat.sub(X,192),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
let H2 = Nat.sub.add.left(192, List.length(U8,payload)) :: rewrite X in Nat.sub(X,192) == List.length(U8,payload) with Nat.add.comm(List.length(U8,payload),192)
replace X with mirror(H2) in Pair.new(Bytes,Bytes,payload,tail) == Nat.lte(X,55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,payload,tail),X),Bytes.split(List.concat(U8,payload,tail),Nat.sub(X,56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
replace X with mirror(H) in Pair.new(Bytes,Bytes,payload,tail) == X(() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,payload,tail),List.length(U8,payload)),Bytes.split(List.concat(U8,payload,tail),Nat.sub(List.length(U8,payload),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))
let split = List.split.length!(payload, tail)
mirror(split)
Ether.RLP.aux.split.3(
payload: Bytes
tail: Bytes
H1: Equal<Bool>(Nat.lte(List.length(U8, payload), 55), false)
H0: Equal<Bool>(Nat.lte(List.length(U8, payload), Ether.RLP.max), true)
): Pair.new(Bytes, Bytes, payload, tail) ==
let b = Bytes.from_nat(List.length!(payload))
let a = Nat.to_u8(Nat.add(56, Nat.add(192, List.length!(b))))
Ether.RLP.split.length(192, a & (b ++ payload) ++ tail)
let bytes_from_nat_length = Ether.RLP.aux.bytes_from_nat(List.length(U8, payload), H0)
let safe_conversion = Nat.to_u8.safe_conversion(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,payload))))), bytes_from_nat_length)
case safe_conversion {
refl:
let concat_assoc = List.concat.assoc(U8,Bytes.from_nat(List.length(U8,payload)),payload,tail)
case concat_assoc {
refl:
let splitted_pair = mirror(List.split.length(U8, Bytes.from_nat(List.length(U8,payload)), List.concat(U8,payload,tail)))
case splitted_pair {
refl:
let recover_length = Bytes.to_nat.from_nat(List.length(U8,payload))
case recover_length {
refl:
mirror(List.split.length(U8, payload, tail))
}: Pair.new(Bytes,Bytes,payload,tail) == List.split(U8,List.concat(U8,payload,tail), recover_length.b)
}: Pair.new(Bytes,Bytes,payload,tail) == splitted_pair.b(() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length)))
}: Pair.new(Bytes,Bytes,payload,tail) == List.split(U8, concat_assoc.b, Nat.sub(Nat.sub(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,payload))))),192),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length)))
}: Pair.new(Bytes,Bytes,payload,tail) == Nat.lte(Nat.sub( safe_conversion.b, 192),55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,payload)),payload),tail),Nat.sub( safe_conversion.b, 192)),Bytes.split(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,payload)),payload),tail),Nat.sub(Nat.sub( safe_conversion.b, 192),56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))))

28
base/Ether/RLP/aux/bytes_from_nat.kind Normal file
View File

@ -0,0 +1,28 @@
Ether.RLP.aux.bytes_from_nat(
n: Nat, H: Nat.lte(n, Nat.pred(Nat.pow(256, 7))) == true
): Nat.lte(List.length(U8, Bytes.from_nat(n)), 7) == true
Ether.RLP.aux.bytes.from_nat.aux(n, 7, H)
Ether.RLP.aux.bytes.from_nat.aux(
n: Nat, m: Nat, H: Nat.lte(n, Nat.pred(Nat.pow(256, m))) == true
): Nat.lte(List.length(U8, Bytes.from_nat(n)), m) == true
case n with H {
zero:
refl
succ:
let concat_length = List.concat.length(U8,Bytes.from_nat(Nat.div(Nat.succ(n.pred),256)),List.cons(U8,U8.from_nat(Nat.mod(Nat.succ(n.pred),256)),List.nil(U8)))
case concat_length {
refl:
case m with H {
zero:
Empty.absurd!(Bool.false_neq_true(H))
succ:
let comm = Nat.add.comm(List.length(U8,List.cons(U8,U8.from_nat(Nat.mod(Nat.succ(n.pred),256)),List.nil(U8))), List.length(U8,Bytes.from_nat(Nat.div(Nat.succ(n.pred),256))))
case comm {
refl:
let ind = Ether.RLP.aux.bytes.from_nat.aux(Nat.div(Nat.succ(n.pred), 256), m.pred, Nat.pow.lte.div_pred(Nat.succ(n.pred), 255, m.pred, H))
ind
}: Equal(Bool, Nat.lte(comm.b,Nat.succ(m.pred)), Bool.true)
}!
}: Equal(Bool, Nat.lte(concat_length.b, m), Bool.true)
}!

2
base/Ether/RLP/bitify/empty.kind
View File

@ -1,2 +0,0 @@
Ether.RLP.bitify.empty: Ether.RLP.Tree<Bits>
Ether.RLP.Tree.tip!(Bits.e)

2
base/Ether/RLP/bitify/nat.kind
View File

@ -1,2 +0,0 @@
Ether.RLP.bifity.nat(n: Nat): Ether.RLP.Tree<Bits>
Ether.RLP.Tree.tip!(Nat.to_bits(n))

2
base/Ether/RLP/bitify/string.kind
View File

@ -1,2 +0,0 @@
Ether.RLP.bitify.string(s: String): Ether.RLP.Tree<Bits>
Ether.RLP.Tree.tip!(String.to_bits(s))

72
base/Ether/RLP/bound_encoding.kind Normal file
View File

@ -0,0 +1,72 @@
Ether.RLP.bound_encoding(
rlps: List<Ether.RLP>, bound: Nat
H: Equal(Bool, Nat.lte(List.length(U8, Ether.RLP.encode.many(rlps)), bound), true)
): Ether.RLP.bound_encoding.type(rlps, bound)
Pair.new!!(
H
case rlps with H {
nil:
unit
cons:
Pair.new!!(
case rlps.head with H {
data:
let split_concat = List.concat.length<U8>(Ether.RLP.encode(Ether.RLP.data(rlps.head.value)), Ether.RLP.encode.many(rlps.tail))
case split_concat with H: Nat.lte(split_concat.b, bound) == true {
refl:
let H = Nat.lte.cut_right(List.length(U8,Ether.RLP.encode(Ether.RLP.data(rlps.head.value))),List.length(U8,Ether.RLP.encode.many(rlps.tail)),bound, H)
def condition = Bool.and(Nat.eql(List.length!(rlps.head.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 127))
case condition with H: Nat.lte(List.length(U8, condition(() Bytes, rlps.head.value, List.concat(U8, Ether.RLP.encode.length(128, List.length(U8, rlps.head.value)), rlps.head.value))), bound) == true {
true:
H
false:
let split_concat = List.concat.length<U8>(Ether.RLP.encode.length(128,List.length(U8,rlps.head.value)), rlps.head.value)
case split_concat with H: Nat.lte(split_concat.b,bound) == Bool.true {
refl:
let H = Nat.lte.cut_left(List.length(U8,Ether.RLP.encode.length(128,List.length(U8,rlps.head.value))),List.length(U8,rlps.head.value),bound, H)
H
}!
}!
}! :: Nat.lte(List.length(U8,rlps.head.value),bound) == true
node:
let split_concat = List.concat.length<U8>(Ether.RLP.encode(Ether.RLP.node(rlps.head.child)), Ether.RLP.encode.many(rlps.tail))
case split_concat with H: Nat.lte(split_concat.b, bound) == true {
refl:
let H = Nat.lte.cut_right(List.length(U8,Ether.RLP.encode(Ether.RLP.node(rlps.head.child))),List.length(U8,Ether.RLP.encode.many(rlps.tail)), bound, H)
let split_concat =
List.concat.length<U8>(Ether.RLP.encode.length(192, List.length(U8, Ether.RLP.encode.many(rlps.head.child))), Ether.RLP.encode.many(rlps.head.child))
case split_concat with H: Nat.lte(split_concat.b, bound) == true {
refl:
let H = Nat.lte.cut_left(List.length(U8,Ether.RLP.encode.length(192,List.length(U8,Ether.RLP.encode.many(rlps.head.child)))),List.length(U8,Ether.RLP.encode.many(rlps.head.child)), bound, H)
Ether.RLP.bound_encoding(rlps.head.child, bound, H)
}!
}! :: Ether.RLP.bound_encoding.type(rlps.head.child,bound)
}! :: rlps.head!!!
let H = H :: Nat.lte(List.length(U8,List.concat(U8, Ether.RLP.encode(rlps.head), Ether.RLP.encode.many(rlps.tail))),bound) == true
case List.concat.length<U8>(Ether.RLP.encode(rlps.head), Ether.RLP.encode.many(rlps.tail)) with H: Nat.lte(self.b, bound) == true {
refl:
let H = Nat.lte.cut_left(List.length(U8, Ether.RLP.encode(rlps.head)), List.length(U8, Ether.RLP.encode.many(rlps.tail)), bound, H)
Ether.RLP.bound_encoding(rlps.tail, bound, H)
}!
)
}! :: rlps!!!
)
Ether.RLP.bound_encoding.type(rlps: List<Ether.RLP>, bound: Nat): Type
And<
Equal<Bool>(Nat.lte(List.length(U8, Ether.RLP.encode.many(rlps)), bound), true)
case rlps {
nil:
Unit
cons:
And<
case rlps.head {
data:
Equal(Bool, Nat.lte(List.length(U8, rlps.head.value), bound), true)
node:
Ether.RLP.bound_encoding.type(rlps.head.child, bound)
}
Ether.RLP.bound_encoding.type(rlps.tail, bound)
>
}
>

41
base/Ether/RLP/decode.kind
View File

@ -1,39 +1,2 @@
Ether.Bits.break(len : Nat, bits : Bits) : Pair<Bits, Bits>
{Bits.take(len, bits), Bits.drop(len, bits)}
Ether.RLP.decode.decode_list(value : Bits) : Pair<List<Ether.RLP.Tree<Bits>>, Bits>
if (Bits.eql(value, Bits.e)) then
{[], value}
else
let {tree, rest} = Ether.RLP.decode(value)
let {trees, rest} = Ether.RLP.decode.decode_list(rest)
{tree & trees, rest}
Ether.RLP.decode(bits : Bits) : Pair<Ether.RLP.Tree<Bits>, Bits>
let {byte_prefix, rest} = Ether.Bits.break(8, bits)
switch (Bits.ltn(byte_prefix)) {
Ether.RLP.Constants.bits_128 :
{Ether.RLP.Tree.tip!(bits), rest}
Ether.RLP.Constants.bits_184 :
let content_length = (Bits.to_nat(byte_prefix) - 128) * 8
let {prefix, rest} = Ether.Bits.break(content_length, rest)
{Ether.RLP.Tree.tip!(prefix), rest}
Ether.RLP.Constants.bits_192 :
let content_length = (Bits.to_nat(byte_prefix) - 183) * 8
let {head, rest} = Ether.Bits.break(content_length, rest)
let length = Ether.RLP.encode.read.binary(head) * 8
let {prefix, rest} = Ether.Bits.break(length*8, rest)
{Ether.RLP.Tree.tip!(prefix), rest}
Ether.RLP.Constants.bits_248 :
let content_length = (Bits.to_nat(byte_prefix) - 192) * 8
let {content, _} = Ether.Bits.break(content_length, rest)
let {xs, rest} = Ether.RLP.decode.decode_list(content)
{Ether.RLP.Tree.list!(xs), rest}
Ether.RLP.Constants.bits_255 :
let content_length = (Bits.to_nat(byte_prefix) - 247) * 8
let {head, rest} = Ether.Bits.break(content_length, rest)
let length = Ether.RLP.encode.read.binary(head) * 8
let {content, _} = Ether.Bits.break(length, rest)
let {xs, rest} = Ether.RLP.decode.decode_list(content)
{Ether.RLP.Tree.list!(xs), rest}
} default {Ether.RLP.Tree.tip!(Bits.e), Bits.e}
Ether.RLP.decode(bytes: Bytes): Ether.RLP
List.head!(Ether.RLP.decode.many(bytes)) <> Ether.RLP.data([])

15
base/Ether/RLP/decode/many.kind Normal file
View File

@ -0,0 +1,15 @@
Ether.RLP.decode.many(bytes: Bytes): List<Ether.RLP>
case bytes {
nil:
[]
cons:
let prefix = U8.to_nat(bytes.head)
if Nat.lte(prefix, 127) then
Ether.RLP.data([bytes.head]) & Ether.RLP.decode.many(bytes.tail)
else if Nat.lte(prefix, 191) then
let {head, tail} = Ether.RLP.split.length(128, bytes)
Ether.RLP.data(head) & Ether.RLP.decode.many(tail)
else
let {head, tail} = Ether.RLP.split.length(192, bytes)
Ether.RLP.node(Ether.RLP.decode.many(head)) & Ether.RLP.decode.many(tail)
}

93
base/Ether/RLP/encode.kind
View File

@ -1,86 +1,11 @@
Ether.RLP.encode(tree : Ether.RLP.Tree<Bits>) : Bits
Ether.RLP.encode(tree: Ether.RLP): Bytes
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
Ether.Bits.pad(8, tree.value)
else
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 128), Ether.Bits.pad(8, tree.value))
list :
let bytes = Bits.e
for item in tree.value with bytes :
Bits.concat(bytes, Ether.RLP.encode(item))
let bytes_size = if Bits.eql(bytes, Bits.e) then
0
else
Ether.Bits.get_bytes_size(bytes)
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 192), bytes)
data:
if Bool.and(Nat.eql(List.length!(tree.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,tree.value))), 127)) then
tree.value
else
List.concat!(Ether.RLP.encode.length(128, List.length!(tree.value)), tree.value)
node:
let rest = Ether.RLP.encode.many(tree.child)
List.concat!(Ether.RLP.encode.length(192, List.length!(rest)), rest)
}
Ether.RPL.proof.encode_length(value : Nat, offSet : Nat) : Bits
switch(Nat.ltn(value)) {
56 :
Ether.Bits.pad(8, Nat.to_bits(value + offSet))
}
default
let binary_encoding = Ether.RPL.proof.encode.binary(value)
let len = Ether.Bits.get_bytes_size(binary_encoding)
let len = Ether.Bits.pad(8, Nat.to_bits(len + offSet + 55))
//log(Bits.show(Nat.to_bits(len + offSet + 55)) | " " | Bits.show(Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)))
Bits.concat.go(len, 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), Ether.Bits.pad(8, Nat.to_bits(value % 256)))
Bits.break(len : Nat, bits : Bits) : Pair<Bits, Bits>
{Bits.take(len, bits), Bits.drop(len, bits)}
Ether.RLP.encode.read.binary(value : Bits) : Nat
let {head, rest} = Bits.break(8, value)
let decode = Bits.to_nat(head)
if (Bits.eql(rest, Bits.e)) then
decode
else
Ether.RLP.encode.read.binary(rest) + (decode * 256)
Ether.RLP.encode.read_list(value : Bits) : Pair<String, Bits>
if (Bits.eql(value, Bits.e)) then
{"" value}
else
let {tree, rest} = Ether.RLP.encode.read(value)
let {trees, rest} = Ether.RLP.encode.read_list(rest)
{tree | trees, rest}
Ether.RLP.encode.read(bits : Bits) : Pair<String, Bits>
let {byte_prefix, rest} = Bits.break(8, bits)
switch (Bits.ltn(byte_prefix)) {
Ether.RLP.Constants.bits_128 :
{String.reverse(Bits.hex.encode(bits)), rest} // 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)), rest}
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.encode.read.binary(head) * 8
let {prefix, rest} = Bits.break(length, rest)
{String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(head))
| String.reverse(Bits.hex.encode(prefix)), rest}
Ether.RLP.Constants.bits_248 :
let content_length = (Bits.to_nat(byte_prefix) - 192) * 8
let {content, rest} = Ether.Bits.break(content_length, rest)
let {xs, _} = Ether.RLP.encode.read_list(content)
{String.reverse(Bits.hex.encode(byte_prefix)) | xs, rest}
Ether.RLP.Constants.bits_255 :
let content_length = (Bits.to_nat(byte_prefix) - 247) * 8
let {head, rest} = Bits.break(content_length, rest)
let length = Ether.RLP.encode.read.binary(head) * 8
let {content, rest} = Ether.Bits.break(length, rest)
let {xs, _} = Ether.RLP.encode.read_list(content)
{String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(head)) | xs, rest}
} default {"", Bits.e}

7
base/Ether/RLP/encode/length.kind Normal file
View File

@ -0,0 +1,7 @@
Ether.RLP.encode.length(add: Nat, length: Nat): Bytes
if Nat.lte(length, 55) then
[Nat.to_u8(Nat.add(add,length))]
else
let b = Bytes.from_nat(length)
let a = Nat.to_u8(Nat.add(56, Nat.add(add, List.length!(b))))
a & b

7
base/Ether/RLP/encode/many.kind Normal file
View File

@ -0,0 +1,7 @@
Ether.RLP.encode.many(trees: List<Ether.RLP>): Bytes
case trees {
nil:
[]
cons:
List.concat!(Ether.RLP.encode(trees.head), Ether.RLP.encode.many(trees.tail))
}

27
base/Ether/RLP/encode_identity.kind Normal file
View File

@ -0,0 +1,27 @@
Ether.RLP.encode_identity(
rlp: Ether.RLP
H: Equal<Bool>(Nat.lte(List.length(U8, Ether.RLP.encode(rlp)), Ether.RLP.max), true)
): Ether.RLP.decode(Ether.RLP.encode(rlp)) == rlp
// first rewrite the bound on the length of the encoding
// so we're able to call the lemma
let H = case List.concat.length(U8, Ether.RLP.encode(rlp), List.nil(U8)) {
refl:
case mirror(Nat.add.zero_right(List.length(U8, Ether.RLP.encode(rlp)))) {
refl:
H
}: Equal<Bool>(Nat.lte(self.b, Ether.RLP.max), true)
}: Equal(Bool, Nat.lte(self.b, Ether.RLP.max), true)
let lemma = Ether.RLP.encode_identity.many([rlp], H)
// simplify concatenation with empty list
let lemma = case mirror(List.concat.nil_right(U8,Ether.RLP.encode(rlp))) {
refl:
lemma
}: Equal(List(Ether.RLP), Ether.RLP.decode.many(self.b), List.cons(Ether.RLP,rlp,List.nil(Ether.RLP)))
let lemma = mirror(lemma)
// substitute lemma inside goal
case lemma {
refl:
refl
}: Equal(Ether.RLP, Maybe.default(Ether.RLP,List.head(Ether.RLP,lemma.b),Ether.RLP.data(List.nil(U8))), rlp)

143
base/Ether/RLP/encode_identity/many.kind Normal file
View File

@ -0,0 +1,143 @@
Ether.RLP.encode_identity.many(
rlps: List<Ether.RLP>
H: Equal<Bool>(Nat.lte(List.length(U8, Ether.RLP.encode.many(rlps)), Ether.RLP.max), true)
): Ether.RLP.decode.many(Ether.RLP.encode.many(rlps)) == rlps
let bound = Ether.RLP.bound_encoding(rlps, Ether.RLP.max, H)
case rlps with bound {
nil:
refl
cons:
bound(
() Ether.RLP.decode.many(Ether.RLP.encode.many(List.cons(Ether.RLP,rlps.head,rlps.tail))) == List.cons(Ether.RLP,rlps.head,rlps.tail)
(bound.fst, bound.snd)
bound.snd(
() Ether.RLP.decode.many(Ether.RLP.encode.many(List.cons(Ether.RLP,rlps.head,rlps.tail))) == List.cons(Ether.RLP,rlps.head,rlps.tail)
(bound.snd.fst, bound.snd.snd)
case rlps.head with bound.snd.fst bound.snd.snd {
data:
let conditions = Bool.and.split(Nat.eql(List.length!(rlps.head.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 127))
def condition = Bool.and(Nat.eql(List.length!(rlps.head.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 127))
case condition with conditions {
true:
case rlps.head.value with conditions {
cons:
case rlps.head.value.tail with conditions {
nil:
open conditions
let conditions.snd = mirror(conditions.snd)
case conditions.snd {
refl:
// data([rlps.head.value.head]) & Ether.RLP.decode.many(Ether.RLP.encode.many(rlps.tail)) == data([rlps.head.value.head]) & rlps.tail
open bound.snd.snd as bound_tail
let ind = Ether.RLP.encode_identity.many(rlps.tail, bound_tail.fst)
apply(List.cons(Ether.RLP, Ether.RLP.data([rlps.head.value.head])), ind)
}: conditions.snd.b( () List(Ether.RLP),List.cons(Ether.RLP,Ether.RLP.data(List.cons(U8,rlps.head.value.head,List.nil(U8))),Ether.RLP.decode.many(List.concat(U8,List.nil(U8),Ether.RLP.encode.many(rlps.tail)))),Nat.lte(U8.to_nat(rlps.head.value.head),191,() List(Ether.RLP),Ether.RLP.split.length(128,List.cons(U8,rlps.head.value.head,List.concat(U8,List.nil(U8),Ether.RLP.encode.many(rlps.tail))),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))),Ether.RLP.split.length(192,List.cons(U8,rlps.head.value.head,List.concat(U8,List.nil(U8),Ether.RLP.encode.many(rlps.tail))),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail))))) == List.cons(Ether.RLP,Ether.RLP.data(List.cons(U8,rlps.head.value.head,List.nil(U8))),rlps.tail)
cons:
open conditions
Empty.absurd!(Bool.false_neq_true(conditions.fst))
}! :: Ether.RLP.decode.many(List.concat(U8,List.cons(U8,rlps.head.value.head,rlps.head.value.tail),Ether.RLP.encode.many(rlps.tail))) == List.cons(Ether.RLP,Ether.RLP.data(List.cons(U8,rlps.head.value.head,rlps.head.value.tail)),rlps.tail)
//?true-278
nil:
open conditions
Empty.absurd!(Bool.false_neq_true(conditions.fst))
}!
false:
//?false-278-10-2370-152742
let size_limit = Equal.refl(Bool, Nat.lte(List.length(U8,rlps.head.value),55))
case Nat.lte(List.length(U8,rlps.head.value),55)
with size_limit: Equal(Bool, Nat.lte(List.length(U8,rlps.head.value),55), self) {
true:
let recover_prefix = Nat.to_u8.safe_conversion(Nat.add(128,List.length(U8,rlps.head.value))
Nat.lte.slack_left(List.length(U8,rlps.head.value), 55, 72, size_limit))
case recover_prefix {
refl:
let limit_size = mirror(Nat.lte.slack_left(List.length(U8,rlps.head.value),55, 8, size_limit))
case limit_size {
refl:
let split_id = Ether.RLP.aux.split.0(rlps.head.value, Ether.RLP.encode.many(rlps.tail), size_limit)
case split_id {
refl:
open bound.snd.snd as bound_tail
let ind = Ether.RLP.encode_identity.many(rlps.tail, bound_tail.fst)
apply(List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value)), ind)
}: split_id.b(() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))) == List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value),rlps.tail)
}: limit_size.b(() List(Ether.RLP),Ether.RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))),Ether.RLP.split.length(192,List.concat(U8,List.concat(U8,Ether.RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail)))) == List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value),rlps.tail)
}: Nat.lte( recover_prefix.b ,127,() List(Ether.RLP),List.cons(Ether.RLP,Ether.RLP.data(List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8))),Ether.RLP.decode.many(List.concat(U8,List.concat(U8,List.nil(U8),rlps.head.value),Ether.RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(Ether.RLP),Ether.RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))),Ether.RLP.split.length(192,List.concat(U8,List.concat(U8,Ether.RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail))))) == List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value),rlps.tail)
// ?true-4418-1090-258-258
false:
let limit_size_length = Ether.RLP.aux.bytes_from_nat(List.length(U8,rlps.head.value), bound.snd.fst)
let recover_prefix = Nat.to_u8.safe_conversion(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))
Nat.lte.slack_left(List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value))), 7, 64, limit_size_length)
)
case recover_prefix {
refl:
let limit_length = mirror(Ether.RLP.aux.bytes_from_nat(List.length(U8,rlps.head.value), bound.snd.fst))
case limit_length {
refl:
let recover_split = Ether.RLP.aux.split.1(rlps.head.value, Ether.RLP.encode.many(rlps.tail), size_limit, bound.snd.fst)
case recover_split {
refl:
open bound.snd.snd as bound_tail
let ind = Ether.RLP.encode_identity.many(rlps.tail, bound_tail.fst)
apply(List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value)), ind)
}: recover_split.b(() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))) == List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value),rlps.tail)
}: limit_length.b( () List(Ether.RLP),Ether.RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value))),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))),Ether.RLP.split.length(192,List.concat(U8,List.concat(U8,Ether.RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail)))) == List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value),rlps.tail)
}: Nat.lte( recover_prefix.b ,127,() List(Ether.RLP),List.cons(Ether.RLP,Ether.RLP.data(List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),List.nil(U8))),Ether.RLP.decode.many(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,rlps.head.value)),rlps.head.value),Ether.RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(Ether.RLP),Ether.RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value))),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))),Ether.RLP.split.length(192,List.concat(U8,List.concat(U8,Ether.RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail))))) == List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value),rlps.tail)
//?false-4418-1090-258-258
}: List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value)))),rlps.head.value),Ether.RLP.encode.many(rlps.tail),(bytes) List(Ether.RLP),List.nil(Ether.RLP),(bytes.head) (bytes.tail) Nat.lte(U8.to_nat(bytes.head),127,() List(Ether.RLP),List.cons(Ether.RLP,Ether.RLP.data(List.cons(U8,bytes.head,List.nil(U8))),Ether.RLP.decode.many(bytes.tail)),Nat.lte(U8.to_nat(bytes.head),191,() List(Ether.RLP),Ether.RLP.split.length(128,List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value)))),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))),Ether.RLP.split.length(192,List.concat(U8,List.concat(U8,Ether.RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),Ether.RLP.encode.many(rlps.tail)),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail)))))) == List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value),rlps.tail)
}! :: Ether.RLP.decode.many(List.concat(U8, condition( () List(U8),rlps.head.value,List.concat(U8,Ether.RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value)),Ether.RLP.encode.many(rlps.tail))) == List.cons(Ether.RLP,Ether.RLP.data(rlps.head.value),rlps.tail)
node:
open bound.snd.fst as bound_child
let ind = Ether.RLP.encode_identity.many(rlps.head.child, bound_child.fst)
let remember_condition = Equal.refl(Bool, Nat.lte(List.length(U8,Ether.RLP.encode.many(rlps.head.child)), 55))
case Nat.lte(List.length(U8,Ether.RLP.encode.many(rlps.head.child)), 55) with remember_condition: Nat.lte(List.length(U8,Ether.RLP.encode.many(rlps.head.child)), 55) == self {
true:
let recover_prefix = Nat.to_u8.safe_conversion(
Nat.add(192,List.length(U8,Ether.RLP.encode.many(rlps.head.child))), Nat.lte.slack_left(List.length(U8,Ether.RLP.encode.many(rlps.head.child)), 55, 8, remember_condition)
)
case recover_prefix {
refl:
let lemma = Ether.RLP.aux.split.2(Ether.RLP.encode.many(rlps.head.child), Ether.RLP.encode.many(rlps.tail), remember_condition)
case lemma {
refl:
open bound.snd.snd as bound_tail
let ind_right = Ether.RLP.encode_identity.many(rlps.tail, bound_tail.fst)
let ind_left = apply(Ether.RLP.node, Ether.RLP.encode_identity.many(rlps.head.child, bound_child.fst))
Equal.vapply(2)!!!!(ind_right)!!!(ind_left, List.cons(Ether.RLP))
}: lemma.b(() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail))) == _
}: Nat.lte( recover_prefix.b ,127,() List(Ether.RLP),List.cons(Ether.RLP,Ether.RLP.data(List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,Ether.RLP.encode.many(rlps.head.child)))),List.nil(U8))),Ether.RLP.decode.many(List.concat(U8,List.concat(U8,List.nil(U8),Ether.RLP.encode.many(rlps.head.child)),Ether.RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(Ether.RLP),Ether.RLP.split.length(128,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,Ether.RLP.encode.many(rlps.head.child)))),List.concat(U8,List.concat(U8,List.nil(U8),Ether.RLP.encode.many(rlps.head.child)),Ether.RLP.encode.many(rlps.tail))),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))),Ether.RLP.split.length(192,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,Ether.RLP.encode.many(rlps.head.child)))),List.concat(U8,List.concat(U8,List.nil(U8),Ether.RLP.encode.many(rlps.head.child)),Ether.RLP.encode.many(rlps.tail))),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail))))) == List.cons(Ether.RLP,Ether.RLP.node(rlps.head.child),rlps.tail)
false:
let bound_bytes_from_nat = Ether.RLP.aux.bytes_from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child)), bound_child.fst)
let recover_prefix =
Nat.to_u8.safe_conversion(
Nat.add(248,List.length(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child)))))
bound_bytes_from_nat
) :: Equal(Nat, Nat.add(248, List.length(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))))), U8.to_nat(Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child)))))))))
case recover_prefix {
refl:
let lemma = Ether.RLP.aux.split.3(Ether.RLP.encode.many(rlps.head.child), Ether.RLP.encode.many(rlps.tail), remember_condition, bound_child.fst)
case lemma {
refl:
open bound.snd.snd as bound_tail
let ind_right = Ether.RLP.encode_identity.many(rlps.tail, bound_tail.fst)
let ind_left = apply(Ether.RLP.node, Ether.RLP.encode_identity.many(rlps.head.child, bound_child.fst))
Equal.vapply(2)!!!!(ind_right)!!!(ind_left, List.cons(Ether.RLP))
}: lemma.b( () List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail))) == List.cons(Ether.RLP,Ether.RLP.node(rlps.head.child),rlps.tail)
}: Nat.lte( recover_prefix.b, 127,() List(Ether.RLP),List.cons(Ether.RLP,Ether.RLP.data(List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))))))),List.nil(U8))),Ether.RLP.decode.many(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))),Ether.RLP.encode.many(rlps.head.child)),Ether.RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(Ether.RLP),Ether.RLP.split.length(128,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))),Ether.RLP.encode.many(rlps.head.child)),Ether.RLP.encode.many(rlps.tail))),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.data(head),Ether.RLP.decode.many(tail))),Ether.RLP.split.length(192,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))),Ether.RLP.encode.many(rlps.head.child)),Ether.RLP.encode.many(rlps.tail))),() List(Ether.RLP),(head) (tail) List.cons(Ether.RLP,Ether.RLP.node(Ether.RLP.decode.many(head)),Ether.RLP.decode.many(tail))))) == List.cons(Ether.RLP,Ether.RLP.node(rlps.head.child),rlps.tail)
}: Ether.RLP.decode.many(List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,Ether.RLP.encode.many(rlps.head.child)))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))))))),Bytes.from_nat(List.length(U8,Ether.RLP.encode.many(rlps.head.child))))),Ether.RLP.encode.many(rlps.head.child)),Ether.RLP.encode.many(rlps.tail))) == List.cons(Ether.RLP,Ether.RLP.node(rlps.head.child),rlps.tail)
}!
)
)
}!

2
base/Ether/RLP/max.kind Normal file
View File

@ -0,0 +1,2 @@
Ether.RLP.max: Nat
Nat.pred(Nat.pow(256, 7))

55
base/Ether/RLP/outdated/decode.kind
View File

@ -1,55 +0,0 @@
String.break(len : Nat, str : String) : Pair<String, String>
{String.take(len, str), String.drop(len, str)}
Ether.RLP.merge_tree(x : List<Ether.RLP.Tree>, y : Ether.RLP.Tree) : Ether.RLP.Tree
case y {
tip : Ether.RLP.Tree.list(y & x)
list : Ether.RLP.Tree.list(y.value ++ x)
}
Ether.RLP.decode.list(encode : String) : Pair<List<Ether.RLP.Tree>, String>
if (String.length(encode) =? 0) || String.eql(encode, "error") then
{[], encode}
else
let {tree, rest} = Ether.RLP.decode.read(encode)
let {trees, rest} = Ether.RLP.decode.list(rest)
{tree & trees, rest}
Ether.RLP.decode.binary(value : String) : Nat
let {head, rest} = String.break(2, value)
let decode = Bits.to_nat(Bits.hex.decode(String.reverse(head)))
if (String.length(rest) =? 0) then
decode
else
Ether.RLP.decode.binary(rest) + (decode * 256)
Ether.RLP.decode.read(encode : String) : Pair<Ether.RLP.Tree, String>
let {prefix, rest} = String.break(2, encode)
let byte_prefix = Bits.hex.decode(String.reverse(prefix))
def bytes_size = String.length(encode)
switch (Bits.ltn(byte_prefix)) {
Ether.RLP.Constants.bits_128 : {Ether.RLP.Tree.tip(byte_prefix), rest} // between (0, 127)
Ether.RLP.Constants.bits_184 :
let content_length = (Bits.to_nat(byte_prefix) - 128) * 2
let {prefix, rest} = String.break(content_length, rest)
{Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
Ether.RLP.Constants.bits_192 :
let content_length = (Bits.to_nat(byte_prefix) - 183) * 2
let {head, rest} = String.break(content_length, rest)
let length = Ether.RLP.decode.binary(head)
let {prefix, rest} = String.break(length *2, rest)
{Ether.RLP.Tree.tip(Bits.hex.decode(String.reverse(prefix))), rest}
Ether.RLP.Constants.bits_248 :
let content_length = (Bits.to_nat(byte_prefix) - 192) * 2
let {xs, rest} = Ether.RLP.decode.list(rest)
{Ether.RLP.Tree.list(xs), rest}
Ether.RLP.Constants.bits_255 :
let content_length = (Bits.to_nat(byte_prefix) - 247) * 2
let {head, rest} = String.break(content_length, rest)
let length = Ether.RLP.decode.binary(head)
let {xs, rest} = Ether.RLP.decode.list(rest)
{Ether.RLP.Tree.list(xs), rest}
} default {Ether.RLP.Tree.list([]), "error"} // treat this case after
Ether.RLP.decode(xs : String) : Ether.RLP.Tree
Pair.fst!!(Ether.RLP.decode.read(String.drop(2, xs)))

43
base/Ether/RLP/outdated/encode.kind
View File

@ -1,43 +0,0 @@
Ether.RLP.encode.bytes(tree : Ether.RLP.Tree) : List<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
Ether.RPL.encode_length(bytes_size, 128) ++ [tree.value]
list :
let bytes = []
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 :
[Nat.to_bits(value + offSet)]
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
// refinements : value <= (2^16) -1
Ether.RPL.encode.binary(value : Nat) : List<Bits>
if (value =? 0) then
[]
else
Ether.RPL.encode.binary(value / 256) ++ [Nat.to_bits(value % 256)]
Ether.RLP.encode.read(bits : List<Bits>) : String
let hexfify = List.map!!((x) String.pad_left(2, '0', String.reverse(Bits.hex.encode(x))), bits)
"0x" | String.join("", hexfify)
Ether.RLP.encode(value : Ether.RLP.Tree) : String
Ether.Bits.read_bytes(Ether.RLP.encode.bytes(value))

186
base/Ether/RLP/section.kind
View File

@ -1,186 +0,0 @@
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.Tree.to_nat(x : Ether.RLP.Tree<Bits>) : Ether.RLP.Tree<Nat>
case x {
list : Ether.RLP.Tree.list!(List.map!!(Ether.RLP.Tree.to_nat, x.value))
tip : Ether.RLP.Tree.tip!(Bits.to_nat(x.value))
}
Nat.complete_diff(x : Nat, y : Nat, H : Nat.lte(x, y) == true) : (x + (y - x)) == y
case x with H {
zero : refl
succ : case y with H {
zero : Empty.absurd!(Bool.false_neq_true(H))
succ :
let rec = Nat.complete_diff(x.pred, y.pred, H)
Equal.apply!!!!(Nat.succ, rec)
}!
}!
Ether.RLP.section.pad_bits8_correctude(value : Bits, H : (Ether.Bits.get_bytes_size(value) =? 1) == true) :
Bits.take(8,Ether.Bits.pad(8,value)) == Ether.Bits.pad(8,value)
let H = Ether.Bits.get_bytes_size.identity_bits_8(value, H)
let simpl = refl :: Nat.eql(Nat.mod(Bits.length(value),8),0,() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value)) == Ether.Bits.pad(8,value)
case simpl {
refl :
(case Nat.eql(Nat.mod(Bits.length(value),8),0) as H {
true : (_) Bits.take.identity(8, value, H)
false : (H1)
let H2 = Nat.Order.trichotomy(Bits.length(value), 8)
let H3 = refl :: Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value) == Bool.false(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value))
case H3 {
refl :
case H2 {
fst :
let absurd = Equal.chain(Bool, true, Nat.lte(Bits.length(value),8), false, Equal.mirror(Bool, Nat.lte(Bits.length(value),8), true, H), H2.value)
Empty.absurd!(Bool.false_neq_true(mirror(absurd)))
snd :
let H1 = Equal.rewrite(Nat, Bits.length(value), 8, H2.value, (Y) Nat.eql(Nat.mod(Y,8),0) == Bool.false, H1)
Empty.absurd!(Bool.false_neq_true(mirror(H1)))
trd :
let H2 = Nat.lte.comm.false(8, Bits.length(value), H2.value)
let H2 = Nat.mod.le_mod(Bits.length(value), 8, H2)
let H2 = Equal.mirror(Nat, Nat.mod(Bits.length(value),8), Bits.length(value), H2)
case H2 {
refl :
let H3 = Nat.complete_diff(Bits.length(value), 8, H)
let H3 = Equal.mirror(Nat, Nat.add(Bits.length(value),Nat.sub(8,Bits.length(value))), 8, H3)
let H4 = Equal.mirror(Nat, Bits.length(Bits.trim(8,value)), 8, Bits.trim.preserve_length(8, value))
let H5 = Bits.take.identity(8, Bits.trim(8,value))
let H6 = refl :: Nat.lte(8, 8) == true
let H6 = H6 :: rewrite X in Nat.lte(X, 8) == Bool.true with H4
let qed = Equal.rewrite(Nat, 8, Nat.add(Bits.length(value),Nat.sub(8,Bits.length(value))), H3, (Y) Bits.take(8,Bits.trim(Y,value)) == Bits.trim(Y,value), H5(H6))
qed
// qed :: rewrite X in Bits.take(8,Bits.trim(X,value)) == Bits.trim(X,value) with H3
} : Bits.take(8,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8, H2.b)),value)) == Bits.trim(Nat.add(Bits.length(value),Nat.sub(8, H2.b)),value)
}
}!
} : (Nat.eql(Nat.mod(Bits.length(value),8),0) == H) -> Bits.take(8,H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value))) == H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value)))(refl)
}!
Ether.RLP.section.tip_case(value : Bits, H : Bits.ltn(value,Ether.RLP.Constants.bits_128) == true, H2 : (Ether.Bits.get_bytes_size(value) =? 1) == true) :
Ether.RLP.Tree.to_nat(Pair.fst(Ether.RLP.Tree(Bits),Bits,Ether.RLP.decode(Ether.Bits.pad(8,value))))
== Ether.RLP.Tree.to_nat(Ether.RLP.Tree.tip(Bits,value))
case refl :: Ether.Bits.break(8,Ether.Bits.pad(8,value),() Pair(Ether.RLP.Tree(Bits),Bits),(byte_prefix) (rest) Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),rest),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),128),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),183),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),247),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e))))))) == Ether.RLP.decode(Ether.Bits.pad(8,value)) {
refl :
case refl :: Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),Bits.drop(8,Ether.Bits.pad(8,value))),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),128),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),183),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),247),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e)))))) == Ether.Bits.break(8,Ether.Bits.pad(8,value),() Pair(Ether.RLP.Tree(Bits),Bits),(byte_prefix) (rest) Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),rest),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),128),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),183),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),247),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e))))))) {
refl :
let pad_id = Ether.RLP.section.pad_bits8_correctude(value, H2)
let pad_id = Equal.mirror(Bits, Bits.take(8,Ether.Bits.pad(8,value)), Ether.Bits.pad(8,value), pad_id)
case pad_id {
refl : ?a
}!
}!
}!
// case Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128) {
// true : ?a
// false : _
// }!
Ether.RLP.section(tree : Ether.RLP.Tree<Bits>) :
Equal(Ether.RLP.Tree<Nat>, Ether.RLP.Tree.to_nat((Pair.fst!!(Ether.RLP.decode(Ether.RLP.encode(tree))))), Ether.RLP.Tree.to_nat(tree))
case tree {
tip :
let e = refl :: Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))) == Ether.RLP.encode(Ether.RLP.Tree.tip(Bits,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 H = Bool.and.eq_sym!!(H)
open H
let H.snd = Equal.mirror(Bool, Bits.ltn(tree.value,Ether.RLP.Constants.bits_128), true, H.snd)
case H.snd {
refl :
let H.fst = Equal.mirror(Bool, Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), Bool.true, H.fst)
case H.fst {
refl : _
}!
} : Ether.RLP.Tree.to_nat(Pair.fst(Ether.RLP.Tree(Bits),Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), H.snd.b,() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value)))))) == Ether.RLP.Tree.to_nat(Ether.RLP.Tree.tip(Bits,tree.value))
false : _
} : Equal(Bool, Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)), self) -> Ether.RLP.Tree.to_nat(Pair.fst(Ether.RLP.Tree(Bits),Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value)))))) == Ether.RLP.Tree.to_nat(Ether.RLP.Tree.tip(Bits,tree.value))
remember(refl)
}!
list : _
}!
// case tree {
// tip :
// let e = refl ::
// Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))) == 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 H = Bool.and.eq_sym!!(H)
// open H
// let H.snd = Equal.mirror(Bool, Bits.ltn(tree.value,Ether.RLP.Constants.bits_128), true, H.snd)
// case H.snd {
// refl :
// let H.fst = Equal.mirror(Bool, Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), Bool.true, H.fst)
// case H.fst {
// refl : ?A-526-142
// } : Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(H.fst.b,Bool.true,() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))))) == Ether.RLP.Tree.tip(tree.value)
// } : Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), H.snd.b,() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))))) == Ether.RLP.Tree.tip(tree.value)
// false : (H) _
// } : Equal(Bool, Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)), self) -> Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))))) == Ether.RLP.Tree.tip(tree.value)
// remember(refl)
// }!
// list : _
// }!
// case tree {
// tip:
// 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:
// ?list_goal
//} : Equal(Ether.RLP.Tree, Ether.RLP.decode(Ether.RLP.encode(tree)), tree)

19
base/Ether/RLP/show.kind
View File

@ -1,11 +1,10 @@
Ether.RLP.to_string(t: List(Ether.RLP.Tree<Bits>)): String
case t {
nil : ""
cons:
"[ " |
case t.head as tree {
tip : Bits.show(tree.value) | ", "
list: Ether.RLP.to_string(t.tail)
}
| " ]"
Ether.RLP.show(r: Ether.RLP): String
case r {
data:
Bytes.to_hex(r.value)
node:
let ret = "["
for child in r.child with ret:
ret|Ether.RLP.show(child)|","
ret|"]"
}

10
base/Ether/RLP/show_list_tree.kind
View File

@ -1,10 +0,0 @@
Ether.RLP.show_list_tree(l: List<Ether.RLP.Tree<Bits>>): String
Ether.RLP.show_list_tree.aux(l, "")
Ether.RLP.show_list_tree.aux(l: List<Ether.RLP.Tree<Bits>>, aux: String): String
case l {
nil : aux
cons:
let s = aux | Ether.RLP.show_tree(l.head)
Ether.RLP.show_list_tree.aux(l.tail, s)
}

5
base/Ether/RLP/show_tree.kind
View File

@ -1,5 +0,0 @@
Ether.RLP.show_tree(t: Ether.RLP.Tree<Bits>): String
case t {
tip : "[" | Bits.show(t.value) | "]"
list: Ether.RLP.show_list_tree(t.value)
}

14
base/Ether/RLP/split.kind Normal file
View File

@ -0,0 +1,14 @@
// Length
// ------
Ether.RLP.split.length(add: Nat, bytes: Bytes): Pair<Bytes, Bytes>
case bytes {
nil:
{[], []}
cons:
let fst = Nat.sub(U8.to_nat(bytes.head), add)
if Nat.lte(fst, 55) then
Bytes.split(bytes.tail, fst)
else
let {length, tail} = Bytes.split(bytes.tail, Nat.sub(fst, 56))
Bytes.split(tail, Bytes.to_nat(length))
}

10
base/Ether/RLP/test/all.kind
View File

@ -1,10 +0,0 @@
RLP.test.all: TestSuite
TestSuite.many("RLP",
[
RLP.test.encode
])
// Show all tests for String
RLP.test.show: _
log(TestSuite.show(RLP.test.all, 0))
0

171
base/Ether/RLP/test/encode.kind
View File

@ -1,171 +0,0 @@
RLP.test.encode: TestSuite
TestSuite.many("RLP.encode", [
RLP.test.encode.0, RLP.test.encode.1, RLP.test.encode.2,
RLP.test.encode.3, RLP.test.encode.4, RLP.test.encode.5,
RLP.test.encode.6, RLP.test.encode.7, RLP.test.encode.8,
RLP.test.encode.9, RLP.test.encode.10, RLP.test.encode.11
])
// zero
RLP.test.encode.0: TestSuite
let test = "0"
let bin = Ether.RPL.encode.binary(0)
let got = Ether.RLP.encode.read(bin)
let exp = "0x80"
let name = "0"
TestSuite.show.log_string(name, test, exp, got)
// Small int
RLP.test.encode.1: TestSuite
let test = "1"
let bin = Ether.RPL.encode.binary(1)
let got = Ether.RLP.encode.read(bin)
let exp = "0x01"
let name = "1"
TestSuite.show.log_string(name, test, exp, got)
// Small int
RLP.test.encode.2: TestSuite
let test = "16"
let bin = Ether.RPL.encode.binary(16)
let got = Ether.RLP.encode.read(bin)
let exp = "0x10"
let name = "2"
TestSuite.show.log_string(name, test, exp, got)
// Small int
RLP.test.encode.3: TestSuite
let test = "79"
let bin = Ether.RPL.encode.binary(79)
let got = Ether.RLP.encode.read(bin)
let exp = "0x4f"
let name = "3"
TestSuite.show.log_string(name, test, exp, got)
// Medium int
RLP.test.encode.4: TestSuite
let test = "100000"
let bin = Ether.RPL.encode.binary(100000)
let got = Ether.RLP.encode.read(bin)
let exp = "0x830186a0"
let name = "4"
TestSuite.show.log_string(name, test, exp, got)
// Medium int
RLP.test.encode.5: TestSuite
let test = "1000"
let bin = Ether.RPL.encode.binary(1000)
let got = Ether.RLP.encode.read(bin)
let exp = "0x8203e8"
let name = "5"
TestSuite.show.log_string(name, test, exp, got)
// Empty list
RLP.test.encode.6: TestSuite
let test = "[]"
// let bin = Ether.RPL.encode.binary(1000)
let got = Ether.RLP.encode.read([])
let exp = "0xc0"
let name = "6"
TestSuite.show.log_string(name, test, exp, got)
// String list
RLP.test.encode.7: TestSuite
let test = "['dog', 'god', 'cat']"
let got = Ether.RLP.encode(RLP.test.list_string)
let exp = "0xcc83646f6783676f6483636174"
let name = "7"
TestSuite.show.log_string(name, test, exp, got)
// List of list
RLP.test.encode.8: TestSuite
let test = "[[[], []], []]"
let got = Ether.RLP.encode(RLP.test.empty)
let exp = "0xc4c2c0c0c0"
let name = "8"
TestSuite.show.log_string(name, test, exp, got)
// multilist
RLP.test.encode.9: TestSuite
let test = "['zw', [4], 1]"
let got = Ether.RLP.encode(RLP.test.multilist)
let exp = "0xc6827a77c10401"
let name = "9"
TestSuite.show.log_string(name, test, exp, got)
RLP.test.encode.10: TestSuite
let test = "dictionary example"
let got = Ether.RLP.encode(RLP.test.dictionary)
let exp = "0xecca846b6579318476616c31ca846b6579328476616c32ca846b6579338476616c33ca846b6579348476616c34"
let name = "10"
TestSuite.show.log_string(name, test, exp, got)
RLP.test.encode.11: TestSuite
let test = "long list"
let got = Ether.RLP.encode(RLP.test.long_list)
let exp = "0xf840cf84617364668471776572847a786376cf84617364668471776572847a786376cf84617364668471776572847a786376cf84617364668471776572847a786376"
let name = "11"
TestSuite.show.log_string(name, test, exp, got)
RLP.test.encode.12: TestSuite
let test = "long string"
let got = Ether.RLP.encode(Ether.RLP.bitify.string(
"Lorem ipsum dolor sit amet, consectetur adipisicing elit"
))
let exp = "0xb8384c6f72656d20697073756d20646f6c6f722073697420616d65742c20636f6e7365637465747572206164697069736963696e6720656c6974"
let name = "12"
TestSuite.show.log_string(name, test, exp, got)
RLP.test.encode.12: TestSuite
let test = "loooong string"
let got = Ether.RLP.encode(Ether.RLP.bitify.string(
"Lorem ipsum dolor sit amet, consectetur adipiscing elit. Curabitur mauris magna, suscipit sed vehicula non, iaculis faucibus tortor. Proin suscipit ultricies malesuada. Duis tortor elit, dictum quis tristique eu, ultrices at risus. Morbi a est imperdiet mi ullamcorper aliquet suscipit nec lorem. Aenean quis leo mollis, vulputate elit varius, consequat enim. Nulla ultrices turpis justo, et posuere urna consectetur nec. Proin non convallis metus. Donec tempor ipsum in mauris congue sollicitudin. Vestibulum ante ipsum primis in faucibus orci luctus et ultrices posuere cubilia Curae; Suspendisse convallis sem vel massa faucibus, eget lacinia lacus tempor. Nulla quis ultricies purus. Proin auctor rhoncus nibh condimentum mollis. Aliquam consequat enim at metus luctus, a eleifend purus egestas. Curabitur at nibh metus. Nam bibendum, neque at auctor tristique, lorem libero aliquet arcu, non interdum tellus lectus sit amet eros. Cras rhoncus, metus ac ornare cursus, dolor justo ultrices metus, at ullamcorper volutpat"
))
let exp = "0xb904004c6f72656d20697073756d20646f6c6f722073697420616d65742c20636f6e73656374657475722061646970697363696e6720656c69742e20437572616269747572206d6175726973206d61676e612c20737573636970697420736564207665686963756c61206e6f6e2c20696163756c697320666175636962757320746f72746f722e2050726f696e20737573636970697420756c74726963696573206d616c6573756164612e204475697320746f72746f7220656c69742c2064696374756d2071756973207472697374697175652065752c20756c7472696365732061742072697375732e204d6f72626920612065737420696d70657264696574206d6920756c6c616d636f7270657220616c6971756574207375736369706974206e6563206c6f72656d2e2041656e65616e2071756973206c656f206d6f6c6c69732c2076756c70757461746520656c6974207661726975732c20636f6e73657175617420656e696d2e204e756c6c6120756c74726963657320747572706973206a7573746f2c20657420706f73756572652075726e6120636f6e7365637465747572206e65632e2050726f696e206e6f6e20636f6e76616c6c6973206d657475732e20446f6e65632074656d706f7220697073756d20696e206d617572697320636f6e67756520736f6c6c696369747564696e2e20566573746962756c756d20616e746520697073756d207072696d697320696e206661756369627573206f726369206c756374757320657420756c74726963657320706f737565726520637562696c69612043757261653b2053757370656e646973736520636f6e76616c6c69732073656d2076656c206d617373612066617563696275732c2065676574206c6163696e6961206c616375732074656d706f722e204e756c6c61207175697320756c747269636965732070757275732e2050726f696e20617563746f722072686f6e637573206e69626820636f6e64696d656e74756d206d6f6c6c69732e20416c697175616d20636f6e73657175617420656e696d206174206d65747573206c75637475732c206120656c656966656e6420707572757320656765737461732e20437572616269747572206174206e696268206d657475732e204e616d20626962656e64756d2c206e6571756520617420617563746f72207472697374697175652c206c6f72656d206c696265726f20616c697175657420617263752c206e6f6e20696e74657264756d2074656c6c7573206c65637475732073697420616d65742065726f732e20437261732072686f6e6375732c206d65747573206163206f726e617265206375727375732c20646f6c6f72206a7573746f20756c747269636573206d657475732c20617420756c6c616d636f7270657220766f6c7574706174"
let name = "12"
TestSuite.show.log_string(name, test, exp, got)
// -- MOCK --
RLP.test.list_string: Ether.RLP.Tree
let bitify_str = (val: String) Ether.RLP.bitify.string(val)
let arr = [bitify_str("dog"), bitify_str("god"), bitify_str("cat")]
Ether.RLP.Tree.list(arr)
// Tree for: ['zw', [4], 1]
RLP.test.multilist: Ether.RLP.Tree
let bitify_str = (val: String) Ether.RLP.bitify.string(val)
let tree_num = (num: Nat) Ether.RLP.Tree.list([Ether.RLP.bifity.nat(num)])
Ether.RLP.Tree.list([bitify_str("zw"), tree_num(4), Ether.RLP.bifity.nat(1)])
// [[[], []], []]
RLP.test.empty: Ether.RLP.Tree
Ether.RLP.Tree.list([
Ether.RLP.Tree.list([Ether.RLP.bitify.empty, Ether.RLP.bitify.empty]),
Ether.RLP.bitify.empty
])
// [["key1", "val1"], ["key2", "val2"], ...]
RLP.test.dictionary: Ether.RLP.Tree
let bitify_str = (val: String) Ether.RLP.bitify.string(val)
let entry = (key: String, val: String) Ether.RLP.Tree.list([bitify_str(key), bitify_str(val)])
Ether.RLP.Tree.list([
entry("key1", "val1"),
entry("key2", "val2"),
entry("key3", "val3"),
entry("key4", "val4")
])
// [["asdf", "qwer", "zxcv"], ["asdf", "qwer", "zxcv"], ...]
RLP.test.long_list: Ether.RLP.Tree
let bitify_str = (val: String) Ether.RLP.bitify.string(val)
let entry = (key: String, val1: String, val2: String) Ether.RLP.Tree.list([bitify_str(key), bitify_str(val1), bitify_str(val2)])
Ether.RLP.Tree.list([
entry("asdf", "qwer", "zxcv"),
entry("asdf", "qwer", "zxcv"),
entry("asdf", "qwer", "zxcv"),
entry("asdf", "qwer", "zxcv")
])
// Reference: https://github.com/ethereumjs/rlp/blob/master/test/fixture/rlptest.json

12
base/Ether/tests.kind
View File

@ -1,10 +1,2 @@
Ether.tests : _
let test = Ether.RLP.Tree.list!([Ether.RLP.Tree.tip!(Nat.to_bits(222222))])
//let list = [test, test, test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test]
// let tree = Ether.RLP.Tree.list(Bits, [Ether.RLP.Tree.list!(list)])
Ether.RLP.encode.read(Ether.RLP.encode(test))
//let buffer = Buffer8.from_hex("d69429d7d1dd5b6f9c864d9db560d72a247c178ae86b0a")
//let hash = Crypto.Keccak.hash.bytes(buffer)
//Buffer8.to_hex(hash)
Ether.tests: _
"Ether.tests"

1
base/List/concat.kind
View File

@ -3,7 +3,6 @@
// as = [3, 4]
// bs = [1, 2]
// List.concat<Nat>(as, bs) == [3, 4, 1, 2]
List.concat<A: Type>(as: List<A>, bs: List<A>): List<A>
case as {
nil: bs,

11
base/List/concat/assoc.kind Normal file
View File

@ -0,0 +1,11 @@
List.concat.assoc<A: Type>(
xs: List<A>,
ys: List<A>,
zs: List<A>
): (xs ++ ys ++ zs) == (xs ++ ys) ++ zs
case xs {
nil: refl
cons: let ind = User.rigille.List.cat_assoc!(xs.tail, ys, zs)
let qed = apply(List.cons<A>(xs.head), ind)
qed
}!

13
base/List/concat/length.kind Normal file
View File

@ -0,0 +1,13 @@
List.concat.length<A: Type>(
l0: List<A>, l1: List<A>
): Equal<Nat>(Nat.add(List.length<A>(l0), List.length<A>(l1)), List.length<A>(List.concat<A>(l0, l1)))
case l0 {
nil:
refl
cons:
let ind = List.concat.length<A>(l0.tail, l1)
case ind {
refl:
refl
}: Equal<Nat>(Nat.succ(Nat.add(List.length<A>(l0.tail), List.length<A>(l1))), Nat.succ(ind.b))
}!

10
base/List/concat/nil_right.kind Normal file
View File

@ -0,0 +1,10 @@
List.concat.nil_right<A: Type>(l: List<A>): l == l ++ []
case l {
nil:
refl
cons:
case List.concat.nil_right<A>(l.tail) {
refl:
refl
}: Equal(List<A>, List.cons(A, l.head, l.tail), List.cons(A, l.head, self.b))
}!

14
base/List/split/length.kind Normal file
View File

@ -0,0 +1,14 @@
List.split.length<A: Type>(
fst: List<A>, snd: List<A>
): List.split<A>(fst ++ snd, List.length<A>(fst)) == Pair.new!!(fst, snd)
case fst {
nil:
refl
cons:
let ind = List.split.length<A>(fst.tail, snd)
def split = List.split(A, fst.tail ++ snd, List.length<A>(fst.tail))
case split with ind: split == Pair.new!!(fst.tail, snd) {
new:
apply((p) open p Pair.new!!(fst.head & p.fst, p.snd), ind)
}! :: split!! == Pair.new!!(fst.head & fst.tail, snd)
}!

14
base/Nat/add/lte.kind Normal file
View File

@ -0,0 +1,14 @@
Nat.add.lte(x : Nat, y : Nat) : Nat.lte(y, Nat.add(x, y)) == true
case x {
succ : case y with {
succ :
let rec = Nat.add.lte(x.pred, y.pred)
let r = Nat.add.succ_both(x.pred, y.pred)
let r = Equal.mirror(Nat, Nat.add(Nat.succ(x.pred),Nat.succ(y.pred)), Nat.succ(Nat.succ(Nat.add(x.pred,y.pred))), r)
case r {
refl : Nat.lte.succ_right!!(rec)
}!
zero : Nat.lte.zero_all(Nat.add(Nat.succ(x.pred),0))
}!
zero : Nat.Order.refl(y)
}!

11
base/Nat/add/sub.kind Normal file
View File

@ -0,0 +1,11 @@
Nat.add.sub(
n: Nat
m: Nat
): Equal<Nat>(Nat.sub(Nat.add(n, m), n), m)
case n {
zero:
refl
succ:
Nat.add.sub(n.pred, m)
}!

2
base/Nat/add/succ_right.kind
View File

@ -1,4 +1,4 @@
Nat.add.succ_right(a: Nat, b: Nat): (a + Nat.succ(b)) == Nat.succ(Nat.add(a,b))
Nat.add.succ_right(a: Nat, b: Nat): Equal(Nat, Nat.add(a, Nat.succ(b)), Nat.succ(Nat.add(a,b)))
case a {
zero: refl
succ:

15
base/Nat/add/swap.kind Normal file
View File

@ -0,0 +1,15 @@
Nat.add.swap(
a: Nat
b: Nat
c: Nat
): Equal(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)))
case Nat.add.assoc(a, b, c) {
refl:
case Nat.add.comm(b, a) {
refl:
case Nat.add.assoc(b, a, c) {
refl:
refl
}: Equal(Nat, Nat.add(Nat.add(b, a), c), self.b)
}: Equal(Nat, Nat.add(self.b, c), Nat.add(b, Nat.add(a, c)))
}: Equal(Nat, self.b, Nat.add(b, Nat.add(a, c)))

9
base/Nat/div/lte.kind Normal file
View File

@ -0,0 +1,9 @@
Nat.div.lte(
a: Nat, b: Nat
H: Equal(Bool, Nat.lte(a, b), true)
): Equal(Nat, 0, Nat.div(a, Nat.succ(b)))
let H = mirror(Nat.lte.comm.true(a, Nat.succ(b), H))
case H {
refl:
refl
}: Equal(Nat, 0, Pair.fst(Nat,Nat,H.b((self) Pair(Nat,Nat),Nat.div_mod.go(Nat.succ(b),1,Nat.sub(a,Nat.succ(b))),Pair.new(Nat,Nat,0,a))))

17
base/Nat/div_mod/go/succ_quotient.kind Normal file
View File

@ -0,0 +1,17 @@
Nat.div_mod.go.succ_quotient(
d: Nat, q: Nat, r: Nat
H: Equal(Bool, Nat.ltn(0, d), true)
): Equal(
Pair(Nat, Nat)
Nat.div_mod.go(d, q, r)(
() Pair(Nat, Nat)
(fst, snd) Pair.new(Nat, Nat, Nat.succ(fst), snd)
)
Nat.div_mod.go(d, Nat.succ(q), r)
)
case Nat.lte(d, r) {
false:
refl
true:
Nat.div_mod.go.succ_quotient(d,Nat.succ(q),Nat.sub(r,d), H)
}: Equal(Pair(Nat, Nat), self(() Pair(Nat,Nat),Nat.div_mod.go(d,Nat.succ(q),Nat.sub(r,d)),Pair.new(Nat,Nat,q,r),() Pair(Nat,Nat),(fst) (snd) Pair.new(Nat,Nat,Nat.succ(fst),snd)), self(() Pair(Nat,Nat),Nat.div_mod.go(d,Nat.succ(Nat.succ(q)),Nat.sub(r,d)),Pair.new(Nat,Nat,Nat.succ(q),r)))

64
base/Nat/div_mod/spec.kind Normal file
View File

@ -0,0 +1,64 @@
// n = r + q*d
// r < n
// --------------
// r = Nat.mod(n, d)
// q = Nat.div(n, d)
Nat.div_mod.spec(
n: Nat
q: Nat
d: Nat
r: Nat
H0: Equal(Nat, n, Nat.add(r, Nat.mul(q, d)))
H1: Equal(Bool, Nat.lte(Nat.succ(r), d), true)
): Equal(Pair<Nat, Nat>, Pair.new(Nat, Nat, q, r), Nat.div_mod(n, d))
case q with H0 {
zero:
let H0 = case Nat.add.zero_right(r) {
refl:
mirror(H0)
}: Equal(Nat, self.b, n)
case H0 {
refl:
let H1 = mirror(Nat.lte.comm.true(r, d, H1))
case H1 {
refl:
refl
}: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,0,r), H1.b((self) Pair(Nat,Nat),Nat.div_mod.go(d,1,Nat.sub(r,d)),Pair.new(Nat,Nat,0,r)))
}: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,0,r), Nat.div_mod(H0.b,d))
succ:
let H1 = mirror(Nat.lte.comm.true(r, d, H1))
let H0 = mirror(H0)
case H0 {
refl:
let pre_cond = mirror(Nat.lte.slack_right(d, d, Nat.add(r,Nat.mul(q.pred,d)), Nat.Order.refl(d)))
let cond = case Nat.add.swap(d, r, Nat.mul(q.pred,d)) {
refl:
pre_cond
}: Equal(Bool, Bool.true, Nat.lte(d, self.b))
case cond {
refl:
let H1 = mirror(H1)
let H1 = Nat.lte.comm.false(d, r, H1)
let succ_out_hyp = Nat.Order.chain(1, Nat.succ(r), d, refl, H1)
let succ_out = Nat.div_mod.go.succ_quotient(d, 0, Nat.sub(n,d), succ_out_hyp)
case succ_out {
refl:
let H0 = mirror(H0)
let H0 = case Nat.add.swap(r, d, Nat.mul(q.pred, d)) {
refl:
H0
}: Equal(Nat, n, self.b)
let H0 = apply((x) Nat.sub(x, d), H0)
let H0 = case Nat.add.sub(d, Nat.add(r, Nat.mul(q.pred, d))) {
refl:
H0
}: Equal(Nat, Nat.sub(n, d), self.b)
let ind = Nat.div_mod.spec(Nat.sub(n, d), q.pred, d, r, H0, H1)
case ind {
refl:
refl
}: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,Nat.succ(q.pred),r), ind.b(() Pair(Nat,Nat),(fst) (snd) Pair.new(Nat,Nat,Nat.succ(fst),snd)))
}: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,Nat.succ(q.pred),r), succ_out.b)
}: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,Nat.succ(q.pred),r), cond.b((self) Pair(Nat,Nat),Nat.div_mod.go(d,1,Nat.sub(n,d)),Pair.new(Nat,Nat,0,n)))
}: Equal(Pair(Nat, Nat), Pair.new(Nat,Nat,Nat.succ(q.pred),r), Nat.lte(d, H0.b,(self) Pair(Nat,Nat),Nat.div_mod.go(d,1,Nat.sub(n,d)),Pair.new(Nat,Nat,0,n)))
}!

13
base/Nat/lte/cut_left.kind Normal file
View File

@ -0,0 +1,13 @@
Nat.lte.cut_left(
a: Nat
b: Nat
c: Nat
H: Equal(Bool, Nat.lte(Nat.add(a, b), c), true)
): Equal(Bool, Nat.lte(b, c), true)
case a with H {
zero:
H
succ:
let lemma = Nat.lte.succ_left(Nat.add(a.pred, b), c, H)
Nat.lte.cut_left(a.pred, b, c, lemma)
}!

10
base/Nat/lte/cut_right.kind Normal file
View File

@ -0,0 +1,10 @@
Nat.lte.cut_right(
a: Nat
b: Nat
c: Nat
H: Equal(Bool, Nat.lte(Nat.add(a, b), c), true)
): Equal(Bool, Nat.lte(a, c), true)
case Nat.add.comm(b, a) with H: Nat.lte(self.b, c) == true {
refl:
Nat.lte.cut_left(b, a, c, H)
}!

15
base/Nat/lte/mul_div.kind Normal file
View File

@ -0,0 +1,15 @@
Nat.lte.mul_div(
a: Nat, b: Nat
H: Equal(Bool, Nat.ltn(0, b), true)
): Equal(Bool, Nat.lte(Nat.mul(b, Nat.div(a, b)), a), true)
let lemma = Nat.div_mod.recover(a, b, H)
case lemma {
refl:
case Nat.mul.comm(b, Nat.div(a,b)) {
refl:
Nat.lte.slack_left(
Nat.mul(b,Nat.div(a,b)), Nat.mul(b,Nat.div(a,b)), Nat.mod(a,b)
Nat.Order.refl(Nat.mul(b,Nat.div(a,b)))
)
}: Equal(Bool, Nat.lte(Nat.mul(b,Nat.div(a,b)),Nat.add(Nat.mod(a,b),self.b)), true)
}: Equal(Bool, Nat.lte(Nat.mul(b, Nat.div(a, b)), lemma.b), true)

11
base/Nat/lte/slack_left.kind Normal file
View File

@ -0,0 +1,11 @@
Nat.lte.slack_left(
a: Nat, b: Nat, c: Nat
H: Equal(Bool, Nat.lte(a, b), true)
): Equal(Bool, Nat.lte(a, Nat.add(c, b)), true)
case c {
zero:
H
succ:
let ind = Nat.lte.slack_left(a, b, c.pred, H)
Nat.lte.succ_right(a, Nat.add(c.pred, b), ind)
}!

9
base/Nat/lte/slack_right.kind Normal file
View File

@ -0,0 +1,9 @@
Nat.lte.slack_right(
a: Nat, b: Nat, c: Nat
H: Equal(Bool, Nat.lte(a, b), true)
): Equal(Bool, Nat.lte(a, Nat.add(b, c)), true)
case Nat.add.comm(c, b) {
refl:
Nat.lte.slack_left(a, b, c, H)
}: Equal(Bool, Nat.lte(a, self.b), true)

14
base/Nat/lte/succ_right.kind Normal file
View File

@ -0,0 +1,14 @@
Nat.lte.succ_right(
x: Nat, y: Nat, H: Nat.lte(x, y) == true
): Nat.lte(x, Nat.succ(y)) == true
case x with H {
zero:
refl
succ:
case y with H {
succ:
Nat.lte.succ_right(x.pred, y.pred, H)
zero:
Empty.absurd!(Bool.false_neq_true(H))
}!
}!

5
base/Nat/lte/zero_all.kind Normal file
View File

@ -0,0 +1,5 @@
Nat.lte.zero_all(y : Nat) : Nat.lte(0, y) == true
case y {
zero : refl
succ : Nat.lte.zero_all(y.pred)
}!

8
base/Nat/ltn.kind
View File

@ -1,8 +1,2 @@
Nat.ltn(n: Nat, m: Nat): Bool
case m {
zero: Bool.false,
succ: case n {
zero: Bool.true,
succ: Nat.ltn(n.pred, m.pred),
}
}
Nat.lte(Nat.succ(n), m)

24
base/Nat/ltn/mul.kind Normal file
View File

@ -0,0 +1,24 @@
Nat.ltn.mul(
a: Nat
b: Nat
c: Nat
H0: Equal(Bool, Nat.ltn(0, c), true)
H1: Equal(Bool, Nat.ltn(a, b), true)
): Equal(Bool, Nat.ltn(Nat.mul(c, a), Nat.mul(c, b)), true)
case c with H0 H1 {
succ:
let H1 = Nat.Order.mul.left(Nat.succ(a), b, Nat.succ(c.pred), H1)
let H1 = case Nat.mul.succ_right(Nat.succ(c.pred), a) {
refl:
H1
}: Equal(Bool, Nat.lte(self.b,Nat.mul(Nat.succ(c.pred),b)), true)
let H1 = H1 :: Equal(Bool, Nat.lte(Nat.succ(Nat.add(c.pred,Nat.mul(Nat.succ(c.pred),a))),Nat.mul(Nat.succ(c.pred),b)), true)
let calc = mirror(Nat.add.succ_right(c.pred, Nat.mul(Nat.succ(c.pred),a)))
let H1 = case calc {
refl:
H1
}: Equal(Bool, Nat.lte(calc.b,Nat.mul(Nat.succ(c.pred),b)), true)
Nat.lte.cut_left(c.pred, Nat.succ(Nat.mul(Nat.succ(c.pred),a)),Nat.mul(Nat.succ(c.pred),b), H1)
zero:
H0
}!

34
base/Nat/ltn/mul_right.kind Normal file
View File

@ -0,0 +1,34 @@
Nat.ltn.mul_right(
a: Nat, b: Nat, c: Nat
H: Equal(Bool, Nat.ltn(a, Nat.mul(b, c)), true)
): Equal(Bool, Nat.ltn(Nat.div(a, b), c), true)
// proof sketch:
// Nat.lte(c, Nat.div(a, b)) is either true or false, suppose it's true
// Nat.lte(b*c, b*Nat.div(a, b))
// Nat.lte(b*c, a) absurd
let b_not_zero = (case b {
zero:
(H)
H
succ:
(H)
refl
}: (H: Equal(Bool, Nat.lte(Nat.succ(a), Nat.mul(b, c)), true)) -> Equal(Bool, Nat.lte(1, b), true))(H)
def cmp = Nat.ltn(Nat.div(a, b), c)
let contra = refl :: Nat.ltn(Nat.div(a, b), c) == Nat.ltn(Nat.div(a, b), c)
case cmp with contra: ^cmp == cmp {
true:
refl
false:
let contra = Nat.lte.comm.false(Nat.succ(Nat.div(a,b)), c, contra)
let contra = contra :: Equal(Bool, Nat.lte(c,Nat.div(a,b)), true)
let contra = Nat.Order.mul.left(c,Nat.div(a,b), b, contra)
let chain_right = Nat.lte.mul_div(a, b, b_not_zero)
let contra = Nat.Order.chain(Nat.mul(b,c), Nat.mul(b,Nat.div(a,b)), a, contra, chain_right)
let H = Nat.lte.comm.true(a,Nat.mul(b,c), H)
let contra = case H {
refl:
contra
}: Equal(Bool, H.b, true)
contra
}!

19
base/Nat/ltn/sub_right.kind Normal file
View File

@ -0,0 +1,19 @@
Nat.ltn.sub_right(
x: Nat, y: Nat, z: Nat
H: Equal(Bool, Nat.ltn(y, Nat.sub(z, x)), true)
): Equal(Bool, Nat.lte(Nat.add(x y), z), true)
case x with H {
succ:
case z with H {
succ:
let H = H :: rewrite X in Nat.lte(Nat.succ(y), X) == Bool.true with (Nat.sub.succ_both(z.pred,x.pred))
let rec = Nat.ltn.sub_right(x.pred, y, z.pred, H)
rec
zero:
let H = H :: Nat.lte(Nat.succ(y),0) == Bool.true
Empty.absurd!(Bool.false_neq_true(H))
}!
zero:
let H = H :: Nat.lte(Nat.succ(y), z) == Bool.true
Nat.lte.succ_left!!(H)
}!

7
base/Nat/mod/go_self.kind
View File

@ -1,7 +0,0 @@
Nat.mod.go_self(a: Nat) (b: Nat): Nat.mod.go(a, a, Nat.succ(b)) == 0
case a{
zero: refl
succ: Nat.mod.go_self(a.pred,Nat.succ(b))
}!

6
base/Nat/mod/idempotent.kind Normal file
View File

@ -0,0 +1,6 @@
Nat.mod.idempotent(x: Nat, y: Nat, H: Nat.lte(y, x) == false): x == Nat.mod(x, y)
let H = mirror(H)
case H {
refl:
refl
}: Equal(Nat, x, Pair.snd(Nat,Nat,H.b((self) Pair(Nat,Nat),Nat.div_mod.go(y,1,Nat.sub(x,y)),Pair.new(Nat,Nat,0,x))))

6
base/Nat/mod/le_mod.kind
View File

@ -1,5 +1,7 @@
Nat.mod.le_mod(x : Nat, y : Nat, H : Nat.lte(Nat.succ(x), y) == true) : Nat.mod(x, y) == x
let simpl = refl :: Pair.snd(Nat,Nat,Nat.lte(y,x,(self) Pair(Nat,Nat),Nat.div_mod.go(y,1,Nat.sub(x,y)),Pair.new(Nat,Nat,0,x))) == Nat.mod(x, y)
Nat.mod.le_mod(
x: Nat, y: Nat, H: Nat.lte(Nat.succ(x), y) == true
): Equal(Nat, Nat.mod(x, y), x)
let simpl = refl :: Pair.snd(Nat,Nat,Nat.lte(y,x,() Pair(Nat,Nat),Nat.div_mod.go(y,1,Nat.sub(x,y)),Pair.new(Nat,Nat,0,x))) == Nat.mod(x, y)
let H2 = Nat.Order.trichotomy(y, x)
case simpl {
refl :

5
base/Nat/mod/mod_one_equals_zero.kind
View File

@ -1,5 +0,0 @@
Nat.mod.mod_one_equals_zero(a: Nat): (a % 1) == 0
case a{
zero: refl
succ: Nat.mod.go_mod_one_equals_zero(a.pred)
}!

28
base/Nat/mod/mul_both.kind Normal file
View File

@ -0,0 +1,28 @@
// a*(b%c) == (a*b)%(a*c)
Nat.mod.mul_both(
a: Nat
b: Nat
c: Nat
H0: Equal(Bool, Nat.lte(1, a), true)
H1: Equal(Bool, Nat.lte(1, c), true)
): Equal(Nat, Nat.mul(a, Nat.mod(b, c)), Nat.mod(Nat.mul(a, b), Nat.mul(a, c)))
let bound_lemma = Nat.lte.comm.false(c, Nat.mod(b, c), Nat.mod.small(b, c, H1))
let bound = Nat.ltn.mul(Nat.mod(b,c), c, a, H0, bound_lemma)
let id_lemma = Nat.div_mod.recover(b, c, H1)
let id_lemma = apply(Nat.mul(a), id_lemma)
let distrib = Nat.mul.distrib_left(a,Nat.mod(b,c),Nat.mul(Nat.div(b,c),c))
let id_lemma = case distrib {
refl:
id_lemma
}: Equal(Nat, distrib.b, Nat.mul(a,b))
let id_lemma = case Nat.mul.swap(a, Nat.div(b,c), c) {
refl:
id_lemma
}: Nat.add(Nat.mul(a,Nat.mod(b,c)), self.b) == Nat.mul(a,b)
// Nat.add(Nat.mul(a,Nat.mod(b,c)),Nat.mul(Nat.div(b,c),Nat.mul(a,c))) == Nat.mul(a,b)
let almost_qed = Nat.div_mod.spec(Nat.mul(a, b), Nat.div(b,c), Nat.mul(a,c), Nat.mul(a,Nat.mod(b,c)), mirror(id_lemma), bound)
let qed = apply(Pair.snd(Nat, Nat), almost_qed)
case qed {
refl:
refl
}: Equal(Nat, Nat.mul(a,Nat.mod(b,c)), qed.b)

3
base/Nat/mod/one.kind Normal file
View File

@ -0,0 +1,3 @@
Nat.mod.one(n: Nat): Equal(Nat, Nat.mod(n, 1), 0)
let lemma = Nat.lte.comm.false(1, Nat.mod(n, 1), Nat.mod.small(n, 1, refl))
Nat.lte.zero_right(Nat.mod(n, 1), lemma)

14
base/Nat/mod/self.kind
View File

@ -1,2 +1,12 @@
Nat.mod.self(a: Nat): (Nat.succ(a) % Nat.succ(a)) == 0
Nat.mod.go_self(a,0)
Nat.mod.self(a: Nat, H: Equal(Bool, Nat.ltn(0, a), true)): Equal(Nat, Nat.mod(a, a), 0)
case Equal.mirror(Bool, Nat.lte(a, a), true, Nat.Order.refl(a)) {
refl:
case Equal.mirror(Nat, Nat.sub(a, a), 0, Nat.sub.cancel(a)) {
refl:
let cond = Equal.mirror(Bool, Nat.lte(a,0), false, Nat.lte.comm.true(0, a, H))
case cond {
refl:
Equal.refl(Nat, 0)
}: Equal(Nat, Pair.snd(Nat,Nat,cond.b(() Pair(Nat,Nat),Nat.div_mod.go(a,2,Nat.sub(0,a)),Pair.new(Nat,Nat,1,0))), 0)
}: Equal(Nat, Pair.snd(Nat,Nat,Nat.div_mod.go(a,1,self.b)), 0)
}: Equal(Nat, Pair.snd(Nat,Nat,self.b(() Pair(Nat,Nat),Nat.div_mod.go(a,1,Nat.sub(a,a)),Pair.new(Nat,Nat,0,a))), 0)

2
base/Nat/mod/small.kind
View File

@ -3,7 +3,7 @@ Nat.mod.small(
m: Nat
Hyp: Equal<Bool>(Nat.lte(1, m), true)
): Equal<Bool>(Nat.lte(m, Nat.mod(n, m)), false)
Nat.mod.small.aux(m,0, n, Hyp)
Nat.mod.small.aux(m, 0, n, Hyp)
Nat.mod.small.aux(
n: Nat

44
base/Nat/mod/succ_left.kind Normal file
View File

@ -0,0 +1,44 @@
Nat.mod.succ_left(
n: Nat, m: Nat
H: Equal(Bool, Nat.lte(m, 0), false)
): Equal(Nat, Nat.mod(Nat.succ(n), m), Nat.mod(Nat.succ(Nat.mod(n, m)), m))
let m_not_zero = Nat.lte.comm.false(m, 0, H)
let H = Nat.div_mod.recover(n, m, m_not_zero)
let H = apply(Nat.succ, H)
let H = mirror(H) :: Equal(Nat, Nat.succ(n), Nat.add(Nat.succ(Nat.mod(n,m)),Nat.mul(Nat.div(n,m),m)))
def cond = Nat.lte(Nat.succ(Nat.succ(Nat.mod(n, m))), m)
let small = refl :: Equal(Bool, cond, cond)
case cond with small: Equal(Bool, ^cond, cond) {
true:
// H: Nat.succ(Nat.add(Nat.mod(n,m),Nat.mul(Nat.div(n,m),m))) == Nat.succ(n)
let lemma = Nat.div_mod.spec(Nat.succ(n), Nat.div(n, m), m, Nat.succ(Nat.mod(n, m)), H, small)
let lemma = apply(Pair.snd(Nat, Nat), lemma)
let lemma = mirror(lemma) :: Equal(Nat, Nat.mod(Nat.succ(n),m), Nat.succ(Nat.mod(n,m)))
case mirror(Nat.mod.le_mod(Nat.succ(Nat.mod(n, m)), m, small)) {
refl:
lemma
}: Equal(Nat, Nat.mod(Nat.succ(n),m), self.b)
false:
let small = Nat.lte.comm.false(Nat.succ(Nat.succ(Nat.mod(n,m))), m, small)
let sandwich = Nat.lte.comm.false(m, Nat.mod(n, m), Nat.mod.small(n, m, m_not_zero))
let equal_m = Nat.Order.anti_symm(Nat.succ(Nat.mod(n, m)), m, sandwich, small)
let H = case equal_m {
refl:
H
}: Equal(Nat, Nat.succ(n), Nat.add(equal_m.b,Nat.mul(Nat.div(n,m),m)))
let H = H :: Equal(Nat, Nat.succ(n), Nat.mul(Nat.succ(Nat.div(n,m)),m))
let lemma = Nat.div_mod.spec(Nat.succ(n), Nat.succ(Nat.div(n, m)), m, 0, H, m_not_zero)
let lemma = apply(Pair.snd(Nat, Nat), lemma) :: Equal(Nat, 0, Nat.mod(Nat.succ(n), m))
case lemma {
refl:
let equal_m = Equal.mirror(Nat, Nat.succ(Nat.mod(n,m)), m, equal_m)
case equal_m {
refl:
case Nat.mod.self(m, m_not_zero) {
refl:
Equal.refl(Nat, Nat.mod(m,m))
}: Equal(Nat, self.b, Nat.mod(m, m))
}: Equal(Nat, 0, Nat.mod(equal_m.b,m))
}: Equal(Nat, lemma.b, Nat.mod(Nat.succ(Nat.mod(n,m)),m))
}!

2
base/Nat/mod/zero_left.kind Normal file
View File

@ -0,0 +1,2 @@
Nat.mod.zero_left(a: Nat): (0 % Nat.succ(a)) == 0
refl

2
base/Nat/mod/zero_mod_equals_zero.kind
View File

@ -1,2 +0,0 @@
Nat.mod.zero_mod_equals_zero(a: Nat): (0 % Nat.succ(a)) == 0
refl

1
base/Nat/mul/assoc.kind
View File

@ -1,3 +1,4 @@
// TODO associative laws are different for addition and multiplication
Nat.mul.assoc(
a: Nat, b: Nat, c: Nat
): Equal<Nat>(Nat.mul(a, Nat.mul(b, c)), Nat.mul(Nat.mul(a, b), c))

15
base/Nat/mul/swap.kind Normal file
View File

@ -0,0 +1,15 @@
Nat.mul.swap(
a: Nat
b: Nat
c: Nat
): Equal(Nat, Nat.mul(a, Nat.mul(b, c)), Nat.mul(b, Nat.mul(a, c)))
case mirror(Nat.mul.assoc(a, b, c)) {
refl:
case Nat.mul.comm(b, a) {
refl:
case mirror(Nat.mul.assoc(b, a, c)) {
refl:
refl
}: Equal(Nat, Nat.mul(Nat.mul(b, a), c), self.b)
}: Equal(Nat, Nat.mul(self.b, c), Nat.mul(b, Nat.mul(a, c)))
}: Equal(Nat, self.b, Nat.mul(b, Nat.mul(a, c)))

2
base/Nat/pow.kind
View File

@ -1,5 +1,5 @@
// x ^ y
Nat.pow(x : Nat, y : Nat) : Nat
Nat.pow(x: Nat, y: Nat): Nat
case y {
zero:
Nat.succ(Nat.zero)

26
base/Nat/pow/lte.kind Normal file
View File

@ -0,0 +1,26 @@
Nat.pow.lte(a: Nat, b: Nat): Equal(Bool, Nat.lte(Nat.pow(Nat.succ(a), b), 0), false)
case b {
zero:
refl
succ:
let remember = Equal.refl(Bool, Nat.lte(Nat.pow(Nat.succ(a), Nat.succ(b.pred)), 0))
def cond = Nat.lte(Nat.pow(Nat.succ(a), Nat.succ(b.pred)), 0)
case cond with remember: cond^ == cond {
true:
let either_zero = Nat.mul.equal_zero(
Nat.succ(a), Nat.pow(Nat.succ(a), b.pred)
Nat.lte.zero_right(Nat.pow(Nat.succ(a), Nat.succ(b.pred)) remember)
)
case either_zero {
left:
apply((n) Bool.not(Nat.is_zero(n)), either_zero.value)
right:
case either_zero.value {
refl:
Nat.pow.lte(a, b.pred)
}: Nat.lte(either_zero.value.b, 0) == false
}
false:
refl
}!
}!

20
base/Nat/pow/lte/div_pred.kind Normal file
View File

@ -0,0 +1,20 @@
Nat.pow.lte.div_pred(
a: Nat, b: Nat, c: Nat, H: Nat.lte(a, Nat.pred(Nat.pow(Nat.succ(b), Nat.succ(c)))) == true
): Equal(Bool, Nat.lte(Nat.div(a, Nat.succ(b)), Nat.pred(Nat.pow(Nat.succ(b), c))), true)
// proof sketch:
// H: succ(a) <= b^(1 + c)
// succ(a) <= b^(1 + c)
// succ(a) <= b*b^c
// a/b < b^c
let H = H :: Equal(Bool, Nat.lte(Nat.succ(a), Nat.succ(Nat.pred(Nat.pow(Nat.succ(b), Nat.succ(c))))), true)
let remove_pred_in = mirror(Nat.succ.pred(Nat.pow(Nat.succ(b), Nat.succ(c)), Nat.lte.comm.false!(0, Nat.pow.lte(b, Nat.succ(c)))))
let remove_pred_out = Nat.succ.pred(Nat.pow(Nat.succ(b), c), Nat.lte.comm.false!(0, Nat.pow.lte(b, c)))
case remove_pred_out {
refl:
let H = case remove_pred_in {
refl:
H
}: Equal(Bool, Nat.lte(Nat.succ(a), remove_pred_in.b), true)
let qed = Nat.ltn.mul_right(a, Nat.succ(b), Nat.pow(Nat.succ(b), c), H)
qed
}: Equal(Bool, Nat.lte(Nat.succ(Nat.div(a, Nat.succ(b))), remove_pred_out.b), true)

2
base/Nat/pow/one_right.kind Normal file
View File

@ -0,0 +1,2 @@
Nat.pow.one_right(n: Nat): n == Nat.pow(n, 1)
mirror(Nat.mul.one_right(n))

41
base/Nat/sub/add.kind
View File

@ -22,3 +22,44 @@ Nat.sub.add(
qed
}!
}!
Nat.sub.add.left(
n: Nat
m: Nat
): Equal<Nat>(Nat.sub(Nat.add(m, n), n), m)
case m {
zero : Nat.sub.cancel(n)
succ :
case n {
zero :
refl :: rewrite X in Nat.succ(X) == Nat.succ(m.pred) with Nat.add.comm(0, m.pred)
succ :
let r = Nat.add.succ_right(m.pred, n.pred)
let rec = Nat.sub.add.left(n.pred, m.pred)
let H1 = Nat.sub.add.left.aux(Nat.add(m.pred,n.pred), n.pred, m.pred, Nat.add.lte(m.pred, n.pred), rec)
case Equal.mirror(Nat, Nat.add(m.pred,Nat.succ(n.pred)), Nat.succ(Nat.add(m.pred,n.pred)), r) as X {
refl : H1
} : Nat.sub(X.b,n.pred) == Nat.succ(m.pred)
}!
}!
Nat.sub.add.left.aux(
m: Nat
n: Nat
z : Nat
H : Nat.lte(n, m) == true
H1 : Equal<Nat>(Nat.sub(m, n), z)) : Equal<Nat>(Nat.sub(Nat.succ(m), n), Nat.succ(z))
case m with H H1 {
succ :
case n with H H1 {
succ : Nat.sub.add.left.aux(m.pred, n.pred, z, H, H1)
zero :
Equal.apply!!!!(Nat.succ, H1)
}!
zero : case n with H H1 {
zero :
Equal.apply!!!!(Nat.succ, H1)
succ :
Empty.absurd!(Bool.false_neq_true(H))
}!
}!

5
base/Nat/sub/cancel.kind Normal file
View File

@ -0,0 +1,5 @@
Nat.sub.cancel(x : Nat) : Nat.sub(x, x) == 0
case x {
zero : refl
succ : Nat.sub.cancel(x.pred)
}!

7
base/Nat/succ/pred.kind Normal file
View File

@ -0,0 +1,7 @@
Nat.succ.pred(n: Nat, H: Nat.ltn(0, n) == true): Equal(Nat, n, Nat.succ(Nat.pred(n)))
case n with H {
zero:
Empty.absurd!(Bool.false_neq_true(H))
succ:
refl
}!

2
base/Nat/to_u8/safe_conversion.kind Normal file
View File

@ -0,0 +1,2 @@
Nat.to_u8.safe_conversion(n: Nat, H: Nat.lte(n, 255) == true): n == U8.to_nat(Nat.to_u8(n))
Word.to_nat.safe(8, n, H)

7
base/Nat/to_word.kind
View File

@ -1,2 +1,7 @@
Nat.to_word(size: Nat, n: Nat): Word(size)
Nat.apply!(n, Word.inc!, Word.zero!)
case n {
zero:
Word.zero(size)
succ:
Word.inc(size, Nat.to_word(size, n.pred))
}!

122
base/RLP.kind
View File

@ -1,122 +0,0 @@
// The RLP format
//
// Serialization and deserialization for the BytesTree type, under the following grammar:
// | First byte | Meaning |
// | ---------- | -------------------------------------------------------------------------- |
// | 0 to 127 | HEX(leaf) |
// | 128 to 183 | HEX(length_of_leaf + 128) + HEX(leaf) |
// | 184 to 191 | HEX(length_of_length_of_leaf + 128 + 56) + HEX(length_of_leaf) + HEX(leaf) |
// | 192 to 247 | HEX(length_of_node + 192) + HEX(node) |
// | 248 to 255 | HEX(length_of_length_of_node + 192 + 56) + HEX(length_of_node) + HEX(node) |
//
// The first byte of RLP.encode.length
// buffer length (len) | RLP.encode.length(add,len)[0]
// ------------------- | -----------------------------
// 56 ~ 256**1-1 | 185
// 256**1 ~ 256**2-1 | 186
// 256**2 ~ 256**3-1 | 187
// 256**3 ~ 256**4-1 | 188
// 256**4 ~ 256**5-1 | 189
// 256**5 ~ 256**6-1 | 190
// 256**6 ~ 256**7-1 | 191
// Type
// ----
type RLP {
data(value: List<U8>)
node(child: List<RLP>)
}
// Length
// ------
RLP.decoder.byte(bytes: Bytes): Pair<Bytes, U8>
case bytes {
nil: {[], 0#8}
cons: {bytes.tail, bytes.head}
}
RLP.encode.length(add: Nat, length: Nat): Bytes
if Nat.ltn(length, 56) then
Bytes.from_nat(Nat.add(add,length))
else
let a = Bytes.from_nat(Nat.add(56, Nat.add(add, RLP.needed_bytes(length))))
let b = Bytes.from_nat(length)
List.concat!(a, b)
RLP.decoder.length(add: Nat, bytes: Bytes): Pair<Bytes, Nat>
case bytes {
nil:
{[], 0}
cons:
let fst = Nat.sub(Bytes.to_nat([bytes.head]), add)
if Nat.ltn(fst, 56) then
{bytes.tail, fst}
else
let {bytes, length} = RLP.decoder.repeat!(RLP.decoder.byte, Nat.sub(fst,56), bytes.tail)
{bytes, Bytes.to_nat(length)}
}
RLP.decode.length(add: Nat, bytes: Bytes): Nat
case RLP.decoder.length(add, bytes) as got {
new: got.snd
}
// Repeat
// ------
RLP.encode.repeat<A: Type>(encode: A -> Bytes, values: List<A>): Bytes
case values {
nil: []
cons: List.concat!(encode(values.head), RLP.encode.repeat<A>(encode, values.tail))
}
RLP.decoder.repeat<A: Type>(decoder: Bytes -> Pair<Bytes,A>, count: Nat, bytes: Bytes): Pair<Bytes, List<A>>
case count {
zero:
{bytes, []}
succ:
let {bytes, head} = decoder(bytes)
let {bytes, tail} = RLP.decoder.repeat<A>(decoder, count.pred, bytes)
{bytes, head & tail}
}
RLP.encode.many(trees: List<RLP>): Bytes
RLP.encode.repeat<RLP>(RLP.encode, trees)
// RLP
// ---
RLP.encode(tree: RLP): Bytes
case tree {
data:
if Bool.and(Nat.eql(List.length!(tree.value),1), U8.ltn(List.head_with_default!(0#8,tree.value), 128#8)) then
tree.value
else
List.concat!(RLP.encode.length(128, List.length!(tree.value)), tree.value)
node:
List.concat!(RLP.encode.length(192, List.length!(tree.child)), RLP.encode.many(tree.child))
}
RLP.decoder(bytes: Bytes): Pair<Bytes, RLP>
case bytes {
nil:
{[], RLP.data([])}
cons:
if U8.ltn(bytes.head, 128#8) then
{List.tail!(bytes), RLP.data([List.head_with_default!(0#8,bytes)])}
else if U8.ltn(bytes.head, 192#8) then
let {bytes, count} = RLP.decoder.length(128, bytes)
let {bytes, value} = RLP.decoder.repeat!(RLP.decoder.byte, count, bytes)
{bytes, RLP.data(value)}
else
let {bytes, count} = RLP.decoder.length(192, bytes)
let {bytes, child} = RLP.decoder.repeat!(RLP.decoder, count, bytes)
{bytes, RLP.node(child)}
}
RLP.decode(bytes: Bytes): RLP
case RLP.decoder(bytes) as got {
new: got.snd
}

184
base/RLP/aux.kind
View File

@ -1,184 +0,0 @@
// These sub-theorems were not proven yet!
// Most of them are simple, and should be finished over the next days
// TODO: include `a <= 192`
RLP.aux.0(
add: Nat
len: Nat
pf0: Either<Equal<Nat, add, 128>, Equal<Nat, add, 192>>
): Nat.ltn(0,Nat.add(add,len)) == Bool.true
RLP.aux.0(add, len, pf0)
// TODO: include `a <= 192`
RLP.aux.1(
a: Nat
n: Nat
e: Equal<Bool, Nat.ltn(n,56), true>
): Equal<Bool, Nat.ltn(Nat.add(a,n), 256), true>
RLP.aux.1(a, n, e)
RLP.aux.2(
n: Nat
e0: Equal<Bool, Nat.ltn(0, n), true>
e1: Equal<Bool, Nat.ltn(n, 256), true>
): Equal<Bytes, Bytes.from_nat(n), [Nat.apply<U8>(n, U8.inc, U8.zero)]>
RLP.aux.2(n, e0, e1)
// TODO: include `a <= 192`
RLP.aux.3(
a: Nat
n: Nat
e: Equal<Bool, Nat.ltn(n,56), true>
): Equal<Bool, Nat.ltn(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(a,n),U8.inc,U8.zero),List.nil(U8))),a),56), true>
RLP.aux.3(a, n, e)
// TODO: include `a <= 192`
RLP.aux.4(
a: Nat
n: Nat
e: Equal<Bool, Nat.ltn(n,56), true>
): Equal<Nat, Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(a,n),U8.inc,U8.zero),List.nil(U8))),a), n>
RLP.aux.4(a, n, e)
// TODO: include `a <= 192`
// TODO: include `n < RLP.max_len` (otherwise this is actually false)
RLP.aux.5(
a: Nat
n: Nat
): Equal<Bool, Nat.ltn(Nat.add(56, Nat.add(a, RLP.needed_bytes(n))), 256), true>
RLP.aux.5(a, n)
// TODO: include `a <= 192`
RLP.aux.6(
a: Nat
n: Nat
): Equal<Bool, Nat.ltn(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(56,Nat.add(a,RLP.needed_bytes(n))),U8.inc,U8.zero),List.nil(U8))),a),56), false>
RLP.aux.6(a, n)
// TODO: include `a <= 192`
RLP.aux.7(
a: Nat
n: Nat
): Equal<Nat, Nat.sub(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(56,Nat.add(a,RLP.needed_bytes(n))),U8.inc,U8.zero),List.nil(U8))),a),56), List.length(U8,Bytes.from_nat(n))>
RLP.aux.7(a, n)
RLP.aux.8(
xs: Bytes
ys: Bytes
): Equal<Pair<Bytes,Bytes>, RLP.decoder.repeat<U8>(RLP.decoder.byte,List.length(U8,xs),List.concat<U8>(xs,ys)), Pair.new!!(ys, xs)>
RLP.aux.8(xs,ys)
RLP.aux.9(
n: Nat
): Equal<Nat, Bytes.to_nat(Bytes.from_nat(n)), n>
RLP.aux.9(n)
RLP.aux.10(
a: Bool
b: Bool
e: Equal<Bool, Bool.and(a,b), true>
): Equal<Bool, a, true>
RLP.aux.10(a, b, e)
RLP.aux.11(
a: Bool
b: Bool
e: Equal<Bool, Bool.and(a,b), true>
): Equal<Bool, b, true>
RLP.aux.11(a, b, e)
RLP.aux.12(
xs: List<U8>
e1: Equal<Bool, Nat.eql(List.length(U8,xs),1), Bool.true>
): Equal<List<U8>, xs, List.cons<U8>(List.head_with_default<U8>(Nat.to_u8(0),xs), List.nil<U8>)>
RLP.aux.12(xs, e1)
RLP.aux.13(
xs: Bytes
ys: Bytes
e0: Nat.eql(List.length(U8,xs),1) == Bool.true
): Equal<Bytes, List.tail(U8,List.concat(U8,xs,ys)), ys>
RLP.aux.13(xs, ys, e0)
RLP.aux.14(
xs: Bytes
ys: Bytes
e0: Nat.eql(List.length(U8,xs),1) == Bool.true
): Equal<Bytes, List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.concat(U8,xs,ys)),List.nil(U8)), xs>
RLP.aux.14(xs, ys, e0)
RLP.aux.15(
x: U8
xs: Bytes
ys: Bytes
zs: Bytes
): Equal<Bytes, List.cons(U8,x,List.concat(U8,List.concat(U8,xs,ys),zs)), List.concat(U8,List.cons(U8,x,xs),List.concat(U8,ys,zs))>
RLP.aux.15(x, xs, ys, zs)
RLP.aux.15.sym(
x: U8
xs: Bytes
ys: Bytes
zs: Bytes
): Equal<Bytes, List.concat(U8,List.cons(U8,x,xs),List.concat(U8,ys,zs)), List.cons(U8,x,List.concat(U8,List.concat(U8,xs,ys),zs))>
mirror(RLP.aux.15(x, xs, ys, zs))
RLP.aux.16(
xs: Bytes
): Equal<Bytes, List.concat<U8>(xs, List.nil<U8>), xs>
case xs {
nil: refl
cons:
let a = RLP.aux.16(xs.tail)
let b = apply(List.cons<U8>(xs.head), a)
b
}!
RLP.aux.17(
len: Nat
): Not<Equal<Bytes, RLP.encode.length(128, len), List.nil(U8)>>
RLP.aux.17(len)
RLP.aux.18(
len: Nat
): Not<Equal<Bytes, RLP.encode.length(192, len), List.nil(U8)>>
RLP.aux.18(len)
RLP.aux.19(
len: Nat
head: U8
tail: Bytes
prof: Equal<Bytes, RLP.encode.length(128,len), List.cons(U8,head,tail)>
): Equal<Bool, U8.ltn(head, 128#8), false>
RLP.aux.19(len, head, tail, prof)
RLP.aux.20(
len: Nat
head: U8
tail: Bytes
prof: Equal<Bytes, RLP.encode.length(128,len), List.cons(U8,head,tail)>
): Equal<Bool, U8.ltn(head, 192#8), true>
RLP.aux.20(len, head, tail, prof)
RLP.aux.21(
len: Nat
head: U8
tail: Bytes
prof: Equal<Bytes, RLP.encode.length(192,len), List.cons(U8,head,tail)>
): Equal<Bool, U8.ltn(head, 128#8), false>
RLP.aux.21(len, head, tail, prof)
RLP.aux.22(
len: Nat
head: U8
tail: Bytes
prof: Equal<Bytes, RLP.encode.length(192,len), List.cons(U8,head,tail)>
): Equal<Bool, U8.ltn(head, 192#8), false>
RLP.aux.22(len, head, tail, prof)
RLP.aux.23<A: Type>(
xs: List<A>
ys: List<A>
zs: List<A>
): Equal<List<A>, List.concat<A>(List.concat<A>(xs,ys),zs), List.concat<A>(xs,List.concat<A>(ys,zs))>
RLP.aux.23<A>(xs, ys, zs)

72
base/RLP/encode_identity.kind
View File

@ -1,72 +0,0 @@
RLP.encode_identity(rlp: RLP): RLP.decode(RLP.encode(rlp)) == rlp
let pf = RLP.encode_identity.go(rlp, [])
let e0 = RLP.aux.16(RLP.encode(rlp))
let e1 = pf :: rewrite X in RLP.decoder(X) == Pair.new(Bytes,RLP,List.nil(U8),rlp) with e0
replace X with mirror(e1) in X((got) RLP,(got.fst) (got.snd) got.snd) == rlp
refl
RLP.encode_identity.go(rlp: RLP, bts: Bytes): Equal<Pair<Bytes,RLP>, RLP.decoder(List.concat<U8>(RLP.encode(rlp),bts)), Pair.new<Bytes,RLP>(bts,rlp)>
let ref_0 = RLP.encode_length_identity.go
let ref_1 = RLP.encode_repeat_identity.go
case rlp {
data:
let e0 = Equal.refl<Bool, Bool.and(Nat.eql(List.length(U8,rlp.value),1),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(128)))>
case Bool.and(Nat.eql(List.length(U8,rlp.value),1),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(128))) as X
with e0 : Equal<Bool, Bool.and(Nat.eql(List.length(U8,rlp.value),1),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(128))), X> {
true:
let e1 = RLP.aux.10(_, _, e0)
let e2 = RLP.aux.11(_, _, e0)
let e3 = RLP.aux.12(rlp.value, e1)
replace X with mirror(e3) in List.concat(U8,X,bts,(bytes) Pair(Bytes,RLP),Pair.new(Bytes,RLP,List.nil(U8),RLP.data(List.nil(U8))),(bytes.head) (bytes.tail) U8.ltn(bytes.head,Nat.to_u8(128),() Pair(Bytes,RLP),Pair.new(List(U8),RLP,List.tail(U8,List.concat(U8,rlp.value,bts)),RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.concat(U8,rlp.value,bts)),List.nil(U8)))),U8.ltn(bytes.head,Nat.to_u8(192),() Pair(Bytes,RLP),RLP.decoder.length(128,List.concat(U8,rlp.value,bts),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.concat(U8,rlp.value,bts),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child))))))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
replace X with mirror(e2) in X(() Pair(Bytes,RLP),Pair.new(List(U8),RLP,List.tail(U8,List.concat(U8,rlp.value,bts)),RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.concat(U8,rlp.value,bts)),List.nil(U8)))),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(192),() Pair(Bytes,RLP),RLP.decoder.length(128,List.concat(U8,rlp.value,bts),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.concat(U8,rlp.value,bts),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e4 = RLP.aux.13(rlp.value, bts, e1)
replace X with mirror(e4) in Pair.new(List(U8),RLP,X,RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.concat(U8,rlp.value,bts)),List.nil(U8)))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e5 = RLP.aux.14(rlp.value, bts, e1)
replace X with mirror(e5) in Pair.new(List(U8),RLP,bts,RLP.data(X)) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
refl
false:
let e1 = Equal.refl<Bytes, RLP.encode.length(128,List.length(U8,rlp.value))>
case RLP.encode.length(128,List.length(U8,rlp.value)) as X
with e1 : Equal<Bytes, RLP.encode.length(128,List.length(U8,rlp.value)), X> {
nil:
let e2 = RLP.aux.17(List.length(U8,rlp.value))
let e3 = e2(e1)
Empty.absurd!(e3)
cons:
let e2 = RLP.aux.19(List.length(U8,rlp.value), X.head, X.tail, e1)
replace X with mirror(e2) in X(() Pair(Bytes,RLP),Pair.new(List(U8),RLP,List.tail(U8,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts))),RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts))),List.nil(U8)))),U8.ltn(X.head,Nat.to_u8(192),() Pair(Bytes,RLP),RLP.decoder.length(128,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e3 = RLP.aux.20(List.length(U8,rlp.value), X.head, X.tail, e1)
replace X with mirror(e3) in X(() Pair(Bytes,RLP),RLP.decoder.length(128,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child))))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e4 = RLP.aux.15.sym(X.head, X.tail, rlp.value, bts)
replace X with e4 in RLP.decoder.length(128,X,() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
replace X with e1 in RLP.decoder.length(128,List.concat(U8,X,List.concat(U8,rlp.value,bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e5 = RLP.encode_length_identity.go(128, List.length<U8>(rlp.value), List.concat(U8,rlp.value,bts), Either.left!!(refl))
replace X with mirror(e5) in X(() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e6 = RLP.aux.8(rlp.value, bts)
replace X with mirror(e6) in X(() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
refl
}: Equal<Pair<Bytes,RLP>, RLP.decoder(List.concat(U8,List.concat(U8,X,rlp.value),bts)), Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))>
} : Equal<Pair<Bytes,RLP>, RLP.decoder(List.concat(U8,X(() List(U8),rlp.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlp.value)),rlp.value)),bts)), Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))>
node:
let e0 = refl
case RLP.encode.length(192,List.length(RLP,rlp.child)) as X
with e0 : Equal<Bytes, RLP.encode.length(192,List.length(RLP,rlp.child)), X> {
nil:
let e1 = RLP.aux.18(List.length(RLP,rlp.child))
let e2 = e1(e0)
Empty.absurd!(e2)
cons:
let e1 = RLP.aux.21(List.length(RLP,rlp.child), X.head, X.tail, e0)
replace X with mirror(e1) in X(() Pair(Bytes,RLP),Pair.new(List(U8),RLP,List.tail(U8,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts))),RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts))),List.nil(U8)))),U8.ltn(X.head,Nat.to_u8(192),() Pair(Bytes,RLP),RLP.decoder.length(128,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
let e2 = RLP.aux.22(List.length(RLP,rlp.child), X.head, X.tail, e0)
replace X with mirror(e2) in X(() Pair(Bytes,RLP),RLP.decoder.length(128,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child))))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
let e3 = RLP.aux.15.sym(X.head, X.tail, RLP.encode.many(rlp.child), bts)
replace X with e3 in RLP.decoder.length(192,X,() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
replace X with e0 in RLP.decoder.length(192,List.concat(U8,X,List.concat(U8,RLP.encode.many(rlp.child),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
let e4 = RLP.encode_length_identity.go(192, List.length(RLP,rlp.child), List.concat(U8,RLP.encode.many(rlp.child),bts), Either.right!!(refl))
replace X with mirror(e4) in X(() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
let e5 = RLP.encode_repeat_identity.go<RLP>(RLP.encode, RLP.decoder, RLP.encode_identity.go, rlp.child, bts)
replace X with mirror(e5) in X(() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
refl
} : RLP.decoder(List.concat(U8,List.concat(U8,X,RLP.encode.many(rlp.child)),bts)) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
}!

32
base/RLP/encode_length_identity.kind
View File

@ -1,32 +0,0 @@
RLP.encode_length_identity.go(
add: Nat
len: Nat
bts: Bytes
pf0: Either<Equal<Nat, add, 128>, Equal<Nat, add, 192>>
): Equal<Pair<Bytes,Nat>, RLP.decoder.length(add,List.concat<U8>(RLP.encode.length(add,len),bts)), Pair.new<Bytes,Nat>(bts,len)>
let e0 = refl
case Nat.ltn(len,56) as X with e0 : Equal<Bool, Nat.ltn(len,56), X> {
true:
let e1 = RLP.aux.0(add, len, pf0)
let e2 = RLP.aux.1(add, len, e0)
let e3 = RLP.aux.2(Nat.add(add,len), e1, e2)
replace X with mirror(e3) in RLP.decoder.length(add,List.concat(U8,X,bts)) == Pair.new(Bytes,Nat,bts,len)
let e4 = RLP.aux.3(add, len, e0)
replace X with mirror(e4) in X(() Pair(Bytes,Nat),Pair.new(List(U8),Nat,List.concat(U8,List.nil(U8),bts),Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(add,len),U8.inc,U8.zero),List.nil(U8))),add)),RLP.decoder.repeat(U8,RLP.decoder.byte,Nat.sub(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(add,len),U8.inc,U8.zero),List.nil(U8))),add),56),List.concat(U8,List.nil(U8),bts),() Pair(Bytes,Nat),(bytes) (length) Pair.new(Bytes,Nat,bytes,Bytes.to_nat(length)))) == Pair.new(Bytes,Nat,bts,len)
let e5 = RLP.aux.4(add, len, e0)
replace X with mirror(e5) in Pair.new(List(U8),Nat,bts,X) == Pair.new(Bytes,Nat,bts,len)
refl
false:
let e1 = RLP.aux.5(add, len)
let e2 = RLP.aux.2(Nat.add(56,Nat.add(add,RLP.needed_bytes(len))), refl, e1)
replace X with mirror(e2) in RLP.decoder.length(add,List.concat(U8,List.concat(U8,X,Bytes.from_nat(len)),bts)) == Pair.new(Bytes,Nat,bts,len)
let e3 = RLP.aux.6(add, len)
replace X with mirror(e3) in X(() Pair(Bytes,Nat),Pair.new(List(U8),Nat,List.concat(U8,List.concat(U8,List.nil(U8),Bytes.from_nat(len)),bts),Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(56,Nat.add(add,RLP.needed_bytes(len))),U8.inc,U8.zero),List.nil(U8))),add)),RLP.decoder.repeat(U8,RLP.decoder.byte,Nat.sub(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(56,Nat.add(add,RLP.needed_bytes(len))),U8.inc,U8.zero),List.nil(U8))),add),56),List.concat(U8,List.concat(U8,List.nil(U8),Bytes.from_nat(len)),bts),() Pair(Bytes,Nat),(bytes) (length) Pair.new(Bytes,Nat,bytes,Bytes.to_nat(length)))) == Pair.new(Bytes,Nat,bts,len)
let e4 = RLP.aux.7(add, len)
replace X with mirror(e4) in RLP.decoder.repeat(U8,RLP.decoder.byte,X,List.concat(U8,List.concat(U8,List.nil(U8),Bytes.from_nat(len)),bts),() Pair(Bytes,Nat),(bytes) (length) Pair.new(Bytes,Nat,bytes,Bytes.to_nat(length))) == Pair.new(Bytes,Nat,bts,len)
let e5 = RLP.aux.8(Bytes.from_nat(len), bts)
replace X with mirror(e5) in X(() Pair(Bytes,Nat),(bytes) (length) Pair.new(Bytes,Nat,bytes,Bytes.to_nat(length))) == Pair.new(Bytes,Nat,bts,len)
let e6 = RLP.aux.9(len)
replace X with mirror(e6) in Pair.new(Bytes,Nat,bts,X) == Pair.new(Bytes,Nat,bts,len)
refl
}: RLP.decoder.length(add,List.concat(U8,X(() Bytes,Bytes.from_nat(Nat.add(add,len)),List.concat(U8,Bytes.from_nat(Nat.add(56,Nat.add(add,RLP.needed_bytes(len)))),Bytes.from_nat(len))),bts)) == Pair.new(Bytes,Nat,bts,len)

21
base/RLP/encode_repeat_identity.kind
View File

@ -1,21 +0,0 @@
RLP.encode_repeat_identity.go<A: Type>(
encode: A -> Bytes
decoder: Bytes -> Pair<Bytes,A>
identity: (val: A, bts: Bytes) -> Equal<Pair<Bytes,A>, decoder(List.concat<U8>(encode(val),bts)), Pair.new<Bytes,A>(bts,val)>
values: List<A>
rest: Bytes
) : def encoded = List.concat<U8>(RLP.encode.repeat<A>(encode, values), rest)
def decoded = RLP.decoder.repeat<A>(decoder, List.length!(values), encoded)
Equal<Pair<Bytes, List<A>>, decoded, Pair.new<Bytes, List<A>>(rest, values)>
case values {
nil:
refl
cons:
let e0 = RLP.aux.23<U8>(encode(values.head), RLP.encode.repeat(A,encode,values.tail), rest)
replace X with mirror(e0) in decoder(X)(() Pair(Bytes,List(A)),(bytes) (head) RLP.decoder.repeat(A,decoder,List.length(A,values.tail),bytes,() Pair(Bytes,List(A)),(bytes) (tail) Pair.new(Bytes,List(A),bytes,List.cons(A,head,tail)))) == Pair.new(Bytes,List(A),rest,List.cons(A,values.head,values.tail))
let e1 = identity(values.head, List.concat<U8>(RLP.encode.repeat(A,encode,values.tail),rest))
replace X with mirror(e1) in X(() Pair(Bytes,List(A)),(bytes) (head) RLP.decoder.repeat(A,decoder,List.length(A,values.tail),bytes,() Pair(Bytes,List(A)),(bytes) (tail) Pair.new(Bytes,List(A),bytes,List.cons(A,head,tail)))) == Pair.new(Bytes,List(A),rest,List.cons(A,values.head,values.tail))
let e2 = RLP.encode_repeat_identity.go<A>(encode, decoder, identity, values.tail, rest)
replace X with mirror(e2) in X(() Pair(Bytes,List(A)),(bytes) (tail) Pair.new(Bytes,List(A),bytes,List.cons(A,values.head,tail))) == Pair.new(Bytes,List(A),rest,List.cons(A,values.head,values.tail))
refl
}!

5
base/RLP/needed_bytes.kind
View File

@ -1,5 +0,0 @@
RLP.needed_bytes(length: Nat): Nat
case length {
zero: 0
succ: Nat.succ(RLP.needed_bytes(Nat.half(Nat.half(Nat.half(Nat.half(Nat.half(Nat.half(Nat.half(Nat.half(length))))))))))
}

18
base/Test.kind
View File

@ -1,18 +1,2 @@
Test: _
Either<String> {
get a = bar([[2]])
get b = foo(a)
return b
}
bar(ll: List<List<Nat>>): Either<String, List<Nat>>
case ll {
nil: Either.left!!("no lists")
cons: Either.right!!(ll.head)
}
foo(l: List<Nat>): Either<String, Nat>
case l {
nil: Either.left!!("empty list")
cons: Either.right!!(l.head)
}
"hello, world!"

11
base/Word/inc.kind
View File

@ -1,6 +1,9 @@
Word.inc<size: Nat>(word: Word(size)): Word(size)
case word {
e: Word.e,
o: Word.i<word.size>(word.pred),
i: Word.o<word.size>(Word.inc<word.size>(word.pred))
} : Word(word.size)
e:
Word.e,
o:
Word.i<word.size>(word.pred),
i:
Word.o<word.size>(Word.inc<word.size>(word.pred))
}: Word(word.size)

13
base/Word/size/succ.kind Normal file
View File

@ -0,0 +1,13 @@
Word.size.succ(n: Nat, w: Word(Nat.succ(n))): w((w, w.size) Type, Empty, (size, pred) Unit, (size, pred) Unit)
let contra = refl :: Nat.succ(n) == Nat.succ(n)
(case w {
e:
(contra)
Empty.absurd!(Nat.succ_neq_zero(n, contra))
o:
(contra)
unit
i:
(contra)
unit
}: (h: Nat.succ(n) == w.size) -> w((k, k.size) Type, Empty, (size, pred) Unit, (size, pred) Unit))(contra)

13
base/Word/size/zero.kind Normal file
View File

@ -0,0 +1,13 @@
Word.size.zero(w: Word(0)): w((w, w.size) Type, Unit, (size, pred) Empty, (size, pred) Empty)
let contra = refl :: 0 == 0
(case w {
e:
(contra)
unit
o:
(contra)
Empty.absurd!(Nat.succ_neq_zero(w.size, contra))
i:
(contra)
Empty.absurd!(Nat.succ_neq_zero(w.size, contra))
}: (h: w.size == 0) -> w((k, k.size) Type, Unit, (size, pred) Empty, (size, pred) Empty))(contra)

9
base/Word/to_nat.kind
View File

@ -1,2 +1,9 @@
Word.to_nat<size: Nat>(word: Word(size)): Nat
Word.fold<(x) Nat, size>(0, <_> Nat.mul(2), <_> (x) Nat.succ(Nat.mul(2, x)), word)
case word {
e:
0
i:
Nat.succ(Nat.mul(2, Word.to_nat(word.size, word.pred)))
o:
Nat.mul(2, Word.to_nat(word.size, word.pred))
}

23
base/Word/to_nat/bound.kind Normal file
View File

@ -0,0 +1,23 @@
Word.to_nat.bound<
size: Nat
>(w: Word(size)
): Equal(Bool, Nat.lte(Nat.succ(Word.to_nat(size, w)), Nat.pow(2, size)), true)
case w {
e:
refl
o:
let ind = Word.to_nat.bound(w.size, w.pred)
let lemma = case Nat.mul.distrib_left(2, 1, Word.to_nat(w.size,w.pred)) {
refl:
Nat.Order.mul.left(Nat.succ(Word.to_nat(w.size,w.pred)), Nat.pow(2,w.size), 2, ind)
}: Equal(Bool, Nat.lte(self.b, Nat.mul(2, Nat.pow(2, w.size))), true)
let qed = Nat.lte.succ_left(Nat.succ(Nat.mul(2, Word.to_nat(w.size,w.pred))), Nat.mul(2, Nat.pow(2,w.size)), lemma)
qed
i:
let ind = Word.to_nat.bound(w.size, w.pred)
let qed = case Nat.mul.distrib_left(2, 1, Word.to_nat(w.size,w.pred)) {
refl:
Nat.Order.mul.left(Nat.succ(Word.to_nat(w.size,w.pred)), Nat.pow(2,w.size), 2, ind)
}: Equal(Bool, Nat.lte(self.b, Nat.mul(2, Nat.pow(2, w.size))), true)
qed
}: Equal(Bool, Nat.lte(Nat.succ(Word.to_nat(w.size, w)), Nat.pow(2, w.size)), true)

59
base/Word/to_nat/from_nat.kind Normal file
View File

@ -0,0 +1,59 @@
Word.to_nat.from_nat<size: Nat>(
n: Nat
): Word.to_nat(size, Nat.to_word(size, n)) == Nat.mod(n, Nat.pow(2, size))
case size {
zero:
let case_elim = Word.size.zero(Nat.to_word(0, n))
let qed =
case Nat.to_word(0, n) {
e:
(case_elim)
case refl :: 1 == Nat.pow(2, 0) {
refl:
case Nat.mod.one(n) {
refl:
refl
}: Equal(Nat, self.b, Nat.mod(n, 1))
}: Equal(Nat, 0, Nat.mod(n, self.b))
i:
(case_elim)
Empty.absurd!(case_elim)
o:
(case_elim)
Empty.absurd!(case_elim)
}: (case_elim: self((w, w.size) Type, Unit, (size, pred) Empty, (size, pred) Empty)) -> (Word.to_nat(self.size, self) == Nat.mod(n, Nat.pow(2, 0)))
qed(case_elim)
succ:
case n {
zero:
let lemma_right =
let contra = Nat.pow.lte(1, Nat.succ(size.pred))
(case Nat.pow(2,Nat.succ(size.pred)) {
zero:
(contra)
Empty.absurd!(Bool.true_neq_false(contra))
succ:
(contra)
refl
}: (contra: Nat.lte(self,0) == Bool.false) -> (0 == Nat.mod(0,self)))(contra)
let lemma_left = mirror(Word.to_nat.zero(Nat.succ(size.pred)))
chain(lemma_left, lemma_right)
succ:
let lemma = refl :: Word.inc(Nat.succ(size.pred),Nat.to_word(Nat.succ(size.pred),n.pred)) == Nat.to_word(Nat.succ(size.pred),Nat.succ(n.pred))
case lemma {
refl:
case Word.to_nat.inc(Nat.succ(size.pred), Nat.to_word(Nat.succ(size.pred), n.pred)) {
refl:
let ind = mirror(Word.to_nat.from_nat(Nat.succ(size.pred), n.pred))
case ind {
refl:
let calc = Nat.mod.succ_left(n.pred,Nat.pow(2,Nat.succ(size.pred)), Nat.pow.lte(1, Nat.succ(size.pred)))
case calc {
refl:
Equal.refl(Nat, Nat.mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(size.pred))))
}: Equal(Nat, calc.b, Nat.mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(size.pred))))
}: Nat.mod(Nat.succ(ind.b),Nat.pow(2,Nat.succ(size.pred))) == Nat.mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(size.pred)))
}: Equal(Nat, self.b, Nat.mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(size.pred))))
}: Equal(Nat, Word.to_nat(Nat.succ(size.pred),lemma.b), Nat.mod(Nat.succ(n.pred),Nat.pow(2,Nat.succ(size.pred))))
}!
}!

53
base/Word/to_nat/inc.kind Normal file
View File

@ -0,0 +1,53 @@
Word.to_nat.inc<
size: Nat
>(w: Word(size)
): Nat.mod(Nat.succ(Word.to_nat(size, w)), Nat.pow(2, size)) == Word.to_nat(size, Word.inc(size, w))
case w {
e:
refl
o:
let calc = refl :: Equal(Nat, Nat.mul(2,Word.to_nat(w.size,w.pred)), Word.to_nat(Nat.succ(w.size),Word.o(w.size,w.pred)))
case calc {
refl:
let pre_bound = Word.to_nat.bound(w.size,w.pred)
let bound = case Nat.mul.distrib_left(2, 1, Word.to_nat(w.size,w.pred)) {
refl:
Nat.Order.mul.left(Nat.succ(Word.to_nat(w.size,w.pred)), Nat.pow(2,w.size), 2, pre_bound)
}: Equal(Bool, Nat.lte(self.b, Nat.mul(2, Nat.pow(2, w.size))), true)
let qed = Nat.mod.le_mod(Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred))),Nat.pow(2,Nat.succ(w.size)), bound)
qed
}: Equal(Nat, Nat.mod(Nat.succ(calc.b),Nat.pow(2,Nat.succ(w.size))), Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred))))
i:
let calc = refl :: Equal(Nat, Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred))), Word.to_nat(Nat.succ(w.size),Word.i(w.size,w.pred)))
case calc {
refl:
let ind = Word.to_nat.inc(w.size, w.pred)
case ind {
refl:
let pow_not_zero = Nat.lte.comm.false(Nat.pow(2,w.size), 0, Nat.pow.lte(1, w.size))
let lemma = Nat.mod.mul_both(2, 1 + Word.to_nat(w.size,w.pred), Nat.pow(2,w.size), refl, pow_not_zero)
let lemma = case Nat.mul.distrib_left(2, 1, Word.to_nat(w.size,w.pred)) {
refl:
lemma
}: Equal(Nat, Nat.mul(2,Nat.mod(Nat.add(1,Word.to_nat(w.size,w.pred)),Nat.pow(2,w.size))), Nat.mod(self.b, Nat.mul(2,Nat.pow(2,w.size))))
let calc = refl :: Equal(Nat, Nat.add(Nat.mul(2,1),Nat.mul(2,Word.to_nat(w.size,w.pred))), Nat.succ(Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred)))))
let lemma = case calc {
refl:
lemma
}: Nat.mul(2,Nat.mod(Nat.add(1,Word.to_nat(w.size,w.pred)),Nat.pow(2,w.size))) == Nat.mod( calc.b, Nat.mul(2,Nat.pow(2,w.size)))
let calc = refl :: Equal(Nat, Nat.mul(2, Nat.pow(2,w.size)), Nat.pow(2,Nat.succ(w.size)))
let lemma = case calc {
refl:
lemma
}: Equal(Nat, Nat.mul(2,Nat.mod(Nat.add(1,Word.to_nat(w.size,w.pred)),Nat.pow(2,w.size))), Nat.mod(Nat.succ(Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred)))), calc.b ))
case lemma {
refl:
let calc = refl :: Equal(Nat, Nat.succ(Word.to_nat(w.size,w.pred)), Nat.add(1,Word.to_nat(w.size,w.pred)))
case calc {
refl:
Equal.refl(Nat, Nat.mul(2,Nat.mod(Nat.succ(Word.to_nat(w.size,w.pred)),Nat.pow(2,w.size))))
}: Equal(Nat, Nat.mul(2,Nat.mod(calc.b,Nat.pow(2,w.size))), Nat.mul(2,Nat.mod(Nat.succ(Word.to_nat(w.size,w.pred)),Nat.pow(2,w.size))))
}: Equal(Nat, lemma.b, Nat.mul(2,Nat.mod(Nat.succ(Word.to_nat(w.size,w.pred)),Nat.pow(2,w.size))))
}: Equal(Nat, Nat.mod(Nat.succ(Nat.succ(Nat.mul(2,Word.to_nat(w.size,w.pred)))),Nat.pow(2,Nat.succ(w.size))), Nat.mul(2,ind.b))
}: Equal(Nat, Nat.mod(Nat.succ(calc.b),Nat.pow(2,Nat.succ(w.size))), Nat.mul(2,Word.to_nat(w.size,Word.inc(w.size,w.pred))))
}: Equal(Nat, Nat.mod(Nat.succ(Word.to_nat(w.size,w)),Nat.pow(2,w.size)), Word.to_nat(w.size,Word.inc(w.size,w)))

7
base/Word/to_nat/safe.kind Normal file
View File

@ -0,0 +1,7 @@
Word.to_nat.safe<size: Nat>(
n: Nat, H: Nat.lte(Nat.succ(n), Nat.pow(2, size)) == true
): n == Word.to_nat(size, Nat.to_word(size, n))
case Nat.mod.le_mod(n, Nat.pow(2, size), H) {
refl:
mirror(Word.to_nat.from_nat(size, n))
}: Equal(Nat, self.b, Word.to_nat(size, Nat.to_word(size, n)))

10
base/Word/to_nat/zero.kind Normal file
View File

@ -0,0 +1,10 @@
Word.to_nat.zero(size: Nat): 0 == Word.to_nat(size, Word.zero(size))
case size {
zero:
refl
succ:
case Word.to_nat.zero(size.pred) {
refl:
refl
}: 0 == Nat.mul(2, self.b)
}!