mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-11-05 07:05:32 +03:00
prove RLP.aux.3
This commit is contained in:
Rígille S. B. Menezes
parent
0d9f0dc30a
commit
6e1684a4cb
@ -38,6 +38,9 @@ Bytes.from_nat(n: Nat): Bytes
|
||||
Bytes.from_nat(n/256) ++ [U8.from_nat(Nat.mod(n, 256))]
|
||||
}
|
||||
|
||||
Bytes.to_nat.from_nat(n: Nat): n == Bytes.to_nat(Bytes.from_nat(n))
|
||||
?bytes.to_nat.from_nat
|
||||
|
||||
Bytes.from_nat.length(n: Nat): Nat.succ(Nat.log2(n)/8) == List.length(U8, Bytes.from_nat(n))
|
||||
?bytes.from_nat.length
|
||||
|
||||
|
||||
11
base/List/concat/assoc.kind
Normal file
11
base/List/concat/assoc.kind
Normal 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
|
||||
}!
|
||||
2
base/Nat/to_u8/safe_conversion.kind
Normal file
2
base/Nat/to_u8/safe_conversion.kind
Normal 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)
|
||||
@ -1,11 +1,6 @@
|
||||
because_i_said_so<A: Type>: A
|
||||
because_i_said_so<A>
|
||||
|
||||
// These sub-theorems were not proven yet!
|
||||
// Most of them are simple, and should be finished over the next days
|
||||
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)
|
||||
|
||||
// These sub-theorems were not proven yet!
|
||||
// Most of them are simple, and should be finished over the next days
|
||||
RLP.aux.split.0(
|
||||
@ -13,18 +8,17 @@ RLP.aux.split.0(
|
||||
tail: Bytes
|
||||
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
|
||||
): Pair.new(Bytes, Bytes, payload, tail) == RLP.split.length(128, Nat.to_u8(Nat.add(128, List.length!(payload))) & payload ++ tail)
|
||||
because_i_said_so!
|
||||
// let chain = Nat.Order.chain(List.length(U8,payload), 55, 126, H, refl)
|
||||
// let H0 = RLP.new_aux.Nat.lte.max_add(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)
|
||||
let chain = Nat.Order.chain(List.length(U8,payload), 55, 126, H, refl)
|
||||
let H0 = RLP.new_aux.Nat.lte.max_add(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)
|
||||
|
||||
RLP.aux.split.1(
|
||||
payload: Bytes
|
||||
@ -41,229 +35,46 @@ RLP.aux.split.2(
|
||||
tail: Bytes
|
||||
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
|
||||
): Pair.new(Bytes, Bytes, payload, tail) == RLP.split.length(192, Nat.to_u8(Nat.add(192, List.length!(payload))) & payload ++ tail)
|
||||
because_i_said_so!
|
||||
// let chain = Nat.Order.chain(List.length(U8,payload), 55, 62, H, refl)
|
||||
// let H0 = RLP.new_aux.Nat.lte.max_add(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)
|
||||
let chain = Nat.Order.chain(List.length(U8,payload), 55, 62, H, refl)
|
||||
let H0 = RLP.new_aux.Nat.lte.max_add(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)
|
||||
|
||||
RLP.aux.split.3(
|
||||
payload: Bytes
|
||||
tail: Bytes
|
||||
H1: Equal<Bool>(Nat.lte(List.length!(payload), 55), false)
|
||||
H0: Equal<Bool>(Nat.lte(List.length!(payload), RLP.max), true)
|
||||
H1: Equal<Bool>(Nat.lte(List.length(U8, payload), 55), false)
|
||||
H0: Equal<Bool>(Nat.lte(List.length(U8, payload), 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))))
|
||||
RLP.split.length(192, a & (b ++ payload) ++ tail)
|
||||
because_i_said_so!
|
||||
// let H1 = mirror(H1)
|
||||
// case H1 {
|
||||
// refl:
|
||||
// let recover_prenum = ?todo.1 :: Nat.add(56, List.length(U8, Bytes.from_nat(List.length(U8, payload)))) == Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,payload))))))),192)
|
||||
// case recover_prenum {
|
||||
// refl:
|
||||
// let recover_bytes = mirror(List.split.length(U8, Bytes.from_nat(List.length(U8,payload)), payload ++ tail))
|
||||
// case recover_bytes {
|
||||
// refl:
|
||||
// let recover_length = ?todo.0 :: List.length(U8, payload) == Bytes.to_nat(Bytes.from_nat(List.length(U8,payload)))
|
||||
// case recover_length {
|
||||
// refl:
|
||||
// List.split.length(U8, payload, tail)
|
||||
// }: Bytes.split(List.concat(U8,payload,tail), recover_length.b ) == Pair.new(Bytes,Bytes,payload,tail)
|
||||
//
|
||||
// }: recover_bytes.b(() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length))) == Pair.new(Bytes,Bytes,payload,tail)
|
||||
//
|
||||
// }: Nat.lte( recover_prenum.b, 55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,Bytes.from_nat(List.length(U8,payload)),List.concat(U8,payload,tail)), recover_prenum.b ),Bytes.split(List.concat(U8,Bytes.from_nat(List.length(U8,payload)),List.concat(U8,payload,tail)),Nat.sub( recover_prenum.b ,56),() Pair(Bytes,Bytes),(length) (tail) Bytes.split(tail,Bytes.to_nat(length)))) == Pair.new(Bytes,Bytes,payload,tail)
|
||||
//
|
||||
// }: RLP.split.length(192,List.concat(U8, H1.b( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,payload))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,payload)))))),Bytes.from_nat(List.length(U8,payload)))),List.concat(U8,payload,tail))) == Pair.new(Bytes,Bytes,payload,tail)
|
||||
let bytes_from_nat_length = 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))))
|
||||
|
||||
RLP.aux.bytes_from_nat(n: Nat, H: Nat.lte(n, RLP.max) == true): Nat.lte(List.length(U8, Bytes.from_nat(n)), 7) == true
|
||||
?RLP.bound.from_nat
|
||||
|
||||
//// 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)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user