mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-11-05 07:05:32 +03:00
get really really close to prove the node case
This commit is contained in:
Rígille S. B. Menezes
parent
4e4dcfdd2a
commit
29ab09c82c
@ -79,7 +79,7 @@ RLP.encode.many(trees: List<RLP>): Bytes
|
||||
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
|
||||
if Bool.and(Nat.eql(List.length!(tree.value),1), Nat.ltn(U8.to_nat((List.head_with_default!(0#8,tree.value))), 128)) then
|
||||
tree.value
|
||||
else
|
||||
List.concat!(RLP.encode.length(128, List.length!(tree.value)), tree.value)
|
||||
|
||||
@ -1,10 +1,14 @@
|
||||
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
|
||||
//RLP.aux.split.0(
|
||||
// payload: Bytes
|
||||
// tail: Bytes
|
||||
// H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
|
||||
//): RLP.split.length(128, RLP.encode.length(128, List.length<U8>(payload)) ++ payload ++ tail) == {payload, tail}
|
||||
RLP.aux.split.0(
|
||||
payload: Bytes
|
||||
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 H = mirror(H)
|
||||
// case H {
|
||||
// refl:
|
||||
@ -19,6 +23,23 @@
|
||||
// }: RLP.split.length(128,List.concat(U8, H.b( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,payload))),List.nil(U8)),List.concat(U8,Bytes.from_nat(Nat.add(56,Nat.add(128,RLP.needed_bytes(List.length(U8,payload))))),Bytes.from_nat(List.length(U8,payload)))),List.concat(U8,payload,tail))) == Pair.new(Bytes,Bytes,payload,tail)
|
||||
|
||||
RLP.aux.split.1(
|
||||
payload: Bytes
|
||||
tail: Bytes
|
||||
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), 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))))
|
||||
RLP.split.length(192, a & (b ++ payload) ++ tail)
|
||||
because_i_said_so!
|
||||
|
||||
RLP.aux.split.2(
|
||||
payload: Bytes
|
||||
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!
|
||||
|
||||
RLP.aux.split.3(
|
||||
payload: Bytes
|
||||
tail: Bytes
|
||||
H1: Equal<Bool>(Nat.lte(List.length!(payload), 55), false)
|
||||
@ -27,7 +48,7 @@ RLP.aux.split.1(
|
||||
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)
|
||||
RLP.aux.split.1(payload, tail, H1, H0)
|
||||
because_i_said_so!
|
||||
// let H1 = mirror(H1)
|
||||
// case H1 {
|
||||
// refl:
|
||||
|
||||
@ -1,6 +1,9 @@
|
||||
typeof<A: Type>(a: A): Type
|
||||
A
|
||||
|
||||
because_i_said_so<A: Type>: A
|
||||
because_i_said_so<A>
|
||||
|
||||
RLP.encode_identity(
|
||||
rlps: List<RLP>
|
||||
H: Equal<Bool>(Nat.lte(List.length(U8, RLP.encode.many(rlps)), RLP.max), true)
|
||||
@ -11,62 +14,83 @@ RLP.encode_identity(
|
||||
cons:
|
||||
case rlps.head {
|
||||
data:
|
||||
?data
|
||||
node:
|
||||
let ind = RLP.encode_identity(rlps.head.child, ?todo.0)
|
||||
case Nat.lte(List.length(U8,RLP.encode.many(rlps.head.child)), 55) {
|
||||
let split_conditions = Bool.and.split(Nat.eql(List.length!(rlps.head.value),1), Nat.ltn(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 128))
|
||||
case Bool.and(Nat.eql(List.length!(rlps.head.value),1), Nat.ltn(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 128)) with split_conditions {
|
||||
true:
|
||||
?true-1110-
|
||||
use conditions = split_conditions(refl)
|
||||
?true
|
||||
false:
|
||||
let recover_prefix = ?todo.1 :: Nat.add(248, List.length(U8,Bytes.from_nat(List.length(U8,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,RLP.encode.many(rlps.head.child))))))))
|
||||
case recover_prefix {
|
||||
refl:
|
||||
let lemma = RLP.aux.split.1(RLP.encode.many(rlps.head.child), RLP.encode.many(rlps.tail), ?todo.2, ?todo.3)
|
||||
case lemma {
|
||||
refl:
|
||||
let ind_right = RLP.encode_identity(rlps.tail, ?todo.4)
|
||||
let ind_left = RLP.encode_identity(rlps.head.child, ?todo.5)
|
||||
?test-258
|
||||
}: lemma.b( () List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
|
||||
|
||||
}: Nat.lte( recover_prefix.b, 127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(RLP),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,RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),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,RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
|
||||
|
||||
//?false-1110-278-70-10
|
||||
|
||||
}: RLP.decode.many(List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,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,RLP.encode.many(rlps.head.child))))))),Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
|
||||
?false
|
||||
}!
|
||||
//?data-22-86-
|
||||
// let remember = Equal.refl(Bool, Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)))
|
||||
// case Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)) as X
|
||||
// with remember : Equal(Bool, Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)), X)
|
||||
// {
|
||||
// true :
|
||||
// let break_and1 = RLP.aux.10!!(remember)
|
||||
// let break_and2 = RLP.aux.11!!(remember)
|
||||
// let ensure_non_empty = RLP.aux.12(rlp.value, break_and1)
|
||||
// replace X with mirror(ensure_non_empty) in Maybe.default(RLP,List.head(RLP,X((bytes) List(RLP),List.nil(RLP),(bytes.head) (bytes.tail) U8.ltn(bytes.head,Nat.to_u8(128),() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,bytes.head,List.nil(U8))),RLP.decode.many(bytes.tail)),U8.ltn(bytes.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
|
||||
// replace X with mirror(break_and2) in Maybe.default(RLP,List.head(RLP,X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),rlp.value),List.nil(U8))),RLP.decode.many(List.nil(U8))),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
|
||||
// let list_length_1 = RlP.new_aux.list_length_1_identity(U8, rlp.value, Nat.to_u8(0), break_and1)
|
||||
// replace X with mirror(list_length_1) in RLP.data(X) == RLP.data(rlp.value)
|
||||
// refl
|
||||
// false :
|
||||
// let list_u8 = 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 list_u8 : Equal(Bytes, RLP.encode.length(128,List.length(U8,rlp.value)), X) {
|
||||
// nil :
|
||||
// let absurd_rlp_length = RLP.aux.17(List.length(U8,rlp.value))
|
||||
// Empty.absurd!(absurd_rlp_length(list_u8))
|
||||
// cons :
|
||||
// let u8_le_128 = RLP.aux.19(List.length(U8,rlp.value), X.head, X.tail, list_u8)
|
||||
// replace X with mirror(u8_le_128) in Maybe.default(RLP,List.head(RLP, X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,X.head,List.nil(U8))),RLP.decode.many(List.concat(U8,X.tail,rlp.value))),U8.ltn(X.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
|
||||
// let u8_le_192 = RLP.aux.20(List.length(U8,rlp.value) X.head, X.tail, list_u8)
|
||||
// replace X with mirror(u8_le_192) in Maybe.default(RLP,List.head(RLP, X(() List(RLP),RLP.split.length(128,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
|
||||
// let e3 = RLP.aux.15.sym(X.head, X.tail)
|
||||
//
|
||||
// ?a-282-
|
||||
// } : RLP.decode(List.concat(U8,X,rlp.value)) == RLP.data(rlp.value)
|
||||
//
|
||||
// } : RLP.decode(X(() List(U8),rlp.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlp.value)),rlp.value))) == RLP.data(rlp.value)
|
||||
//?data
|
||||
node:
|
||||
because_i_said_so!
|
||||
// let ind = RLP.encode_identity(rlps.head.child, ?todo.0)
|
||||
// case Nat.lte(List.length(U8,RLP.encode.many(rlps.head.child)), 55) {
|
||||
// true:
|
||||
// let recover_prefix = ?todo.5 :: Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child))) == U8.to_nat(Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))))
|
||||
// case recover_prefix {
|
||||
// refl:
|
||||
// let lemma = RLP.aux.split.2(RLP.encode.many(rlps.head.child), RLP.encode.many(rlps.tail), ?todo.2)
|
||||
// case lemma {
|
||||
// refl:
|
||||
// let ind_right = RLP.encode_identity(rlps.tail, ?todo.7)
|
||||
// let ind_left = apply(RLP.node, RLP.encode_identity(rlps.head.child, ?todo.8))
|
||||
// Equal.vapply(2)!!!!(ind_right)!!!(ind_left, List.cons(RLP))
|
||||
// }: lemma.b(() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))) == _
|
||||
//
|
||||
// }: Nat.lte( recover_prefix.b ,127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(RLP),RLP.split.length(128,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.concat(U8,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.concat(U8,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
|
||||
//
|
||||
// false:
|
||||
// let recover_prefix = ?todo.1 :: Nat.add(248, List.length(U8,Bytes.from_nat(List.length(U8,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,RLP.encode.many(rlps.head.child))))))))
|
||||
// case recover_prefix {
|
||||
// refl:
|
||||
// let lemma = RLP.aux.split.3(RLP.encode.many(rlps.head.child), RLP.encode.many(rlps.tail), ?todo.2, ?todo.3)
|
||||
// case lemma {
|
||||
// refl:
|
||||
// let ind_right = RLP.encode_identity(rlps.tail, ?todo.4)
|
||||
// let ind_left = apply(RLP.node, RLP.encode_identity(rlps.head.child, ?todo.5))
|
||||
// Equal.vapply(2)!!!!(ind_right)!!!(ind_left, List.cons(RLP))
|
||||
//
|
||||
// }: lemma.b( () List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
|
||||
//
|
||||
// }: Nat.lte( recover_prefix.b, 127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(RLP),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,RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),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,RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
|
||||
//
|
||||
// }: RLP.decode.many(List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,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,RLP.encode.many(rlps.head.child))))))),Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
|
||||
}!
|
||||
}!
|
||||
|
||||
// let remember = Equal.refl(Bool, Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)))
|
||||
// case Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)) as X
|
||||
// with remember : Equal(Bool, Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)), X)
|
||||
// {
|
||||
// true :
|
||||
// let break_and1 = RLP.aux.10!!(remember)
|
||||
// let break_and2 = RLP.aux.11!!(remember)
|
||||
// let ensure_non_empty = RLP.aux.12(rlp.value, break_and1)
|
||||
// replace X with mirror(ensure_non_empty) in Maybe.default(RLP,List.head(RLP,X((bytes) List(RLP),List.nil(RLP),(bytes.head) (bytes.tail) U8.ltn(bytes.head,Nat.to_u8(128),() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,bytes.head,List.nil(U8))),RLP.decode.many(bytes.tail)),U8.ltn(bytes.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
|
||||
// replace X with mirror(break_and2) in Maybe.default(RLP,List.head(RLP,X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),rlp.value),List.nil(U8))),RLP.decode.many(List.nil(U8))),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
|
||||
// let list_length_1 = RlP.new_aux.list_length_1_identity(U8, rlp.value, Nat.to_u8(0), break_and1)
|
||||
// replace X with mirror(list_length_1) in RLP.data(X) == RLP.data(rlp.value)
|
||||
// refl
|
||||
// false :
|
||||
// let list_u8 = 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 list_u8 : Equal(Bytes, RLP.encode.length(128,List.length(U8,rlp.value)), X) {
|
||||
// nil :
|
||||
// let absurd_rlp_length = RLP.aux.17(List.length(U8,rlp.value))
|
||||
// Empty.absurd!(absurd_rlp_length(list_u8))
|
||||
// cons :
|
||||
// let u8_le_128 = RLP.aux.19(List.length(U8,rlp.value), X.head, X.tail, list_u8)
|
||||
// replace X with mirror(u8_le_128) in Maybe.default(RLP,List.head(RLP, X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,X.head,List.nil(U8))),RLP.decode.many(List.concat(U8,X.tail,rlp.value))),U8.ltn(X.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
|
||||
// let u8_le_192 = RLP.aux.20(List.length(U8,rlp.value) X.head, X.tail, list_u8)
|
||||
// replace X with mirror(u8_le_192) in Maybe.default(RLP,List.head(RLP, X(() List(RLP),RLP.split.length(128,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
|
||||
// let e3 = RLP.aux.15.sym(X.head, X.tail)
|
||||
//
|
||||
// ?a-282-
|
||||
// } : RLP.decode(List.concat(U8,X,rlp.value)) == RLP.data(rlp.value)
|
||||
//
|
||||
// } : RLP.decode(X(() List(U8),rlp.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlp.value)),rlp.value))) == RLP.data(rlp.value)
|
||||
|
||||
// let pf = RLP.encode_identity.go(rlp, [])
|
||||
// let e0 = RLP.aux.16(RLP.encode(rlp))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user