mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-11-05 07:05:32 +03:00
Recursive Length Prefix (RLP): encoder, decoder and identity proof
This commit is contained in:
MaiaVictor
parent
85cbac15c1
commit
d87ada0334
122
base/RLP.kind
Normal file
122
base/RLP.kind
Normal file
@ -0,0 +1,122 @@
|
||||
// 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
|
||||
}
|
||||
|
||||
// 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
|
||||
}
|
||||
|
||||
// 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)
|
||||
181
base/RLP/aux.kind
Normal file
181
base/RLP/aux.kind
Normal file
@ -0,0 +1,181 @@
|
||||
// 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
Normal file
72
base/RLP/encode_identity.kind
Normal file
@ -0,0 +1,72 @@
|
||||
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))
|
||||
}!
|
||||
|
||||
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
|
||||
32
base/RLP/encode_length_identity.kind
Normal file
32
base/RLP/encode_length_identity.kind
Normal file
@ -0,0 +1,32 @@
|
||||
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
Normal file
21
base/RLP/encode_repeat_identity.kind
Normal file
@ -0,0 +1,21 @@
|
||||
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
Normal file
5
base/RLP/needed_bytes.kind
Normal file
@ -0,0 +1,5 @@
|
||||
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))))))))))
|
||||
}
|
||||
@ -1,8 +1,2 @@
|
||||
Test: _
|
||||
Kindelia.hash_code("oi tudo bem? aaa", 0)
|
||||
|
||||
Kindelia.hash_code(str: String, hash: U32): U32
|
||||
case str {
|
||||
nil: hash
|
||||
cons: Kindelia.hash_code(str.tail, (U32.shl(hash, 5) - hash) + U16.to_u32(str.head))
|
||||
}
|
||||
RLP.encode.length(128, Nat.pow(256,7))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user