Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-11-05 07:05:32 +03:00
Code Issues Projects Releases Wiki Activity

make holes in node case purely arithmetical

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-23 09:54:57 -03:00
parent e6ba12c22c
commit 30003dd12c
6 changed files with 39 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
base/Bytes.kind
View File

@ -38,7 +38,7 @@ Bytes.from_nat(n: Nat): Bytes
Bytes.from_nat(n/256) ++ [U8.from_nat(Nat.mod(n, 256))]
}
Bytes.from_nat.length(n: Nat): Nat.log2(Nat.succ(n))/8 == List.length(U8, Bytes.from_nat(n))
Bytes.from_nat.length(n: Nat): Nat.succ(Nat.log2(n)/8) == List.length(U8, Bytes.from_nat(n))
?bytes.from_nat.length
Bytes.to_hex(b: Bytes): String

2
base/Nat/log2/bound.kind Normal file
View File

@ -0,0 +1,2 @@
Nat.log2.bound.up(n: Nat, m: Nat, H: Nat.lte(Nat.succ(n), Nat.pow(2, m)) == true): Nat.lte(Nat.succ(Nat.log2(n)), m) == true
?nat.log2.bound.up

2
base/RLP.kind
View File

@ -105,7 +105,7 @@ RLP.decode.many(bytes: Bytes): List<RLP>
}
RLP.max: Nat
Nat.sub(Nat.pow(256, 7), 1)
Nat.sub(Nat.pow(2, Nat.mul(8, 7)), 1)
RLP.decode(bytes: Bytes): RLP
List.head!(RLP.decode.many(bytes)) <> RLP.data([])

49
base/RLP/aux.kind
View File

@ -3,8 +3,8 @@ because_i_said_so<A: Type>: 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(x : Nat, H : Nat.lte(x, 255) == true) : x == U8.to_nat(Nat.to_u8(x))
because_i_said_so!
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
@ -13,17 +13,18 @@ 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)
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)
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)
RLP.aux.split.1(
payload: Bytes
@ -40,15 +41,16 @@ 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)
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)
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)
RLP.aux.split.3(
payload: Bytes
@ -81,6 +83,9 @@ RLP.aux.split.3(
//
// }: 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)
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

7
base/RLP/encode_identity.kind
View File

@ -114,7 +114,12 @@ RLP.encode_identity(
}: 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 = Nat.to_u8.safe_conversion(Nat.add(248, List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))), ?todo.1)
let bound_bytes_from_nat = RLP.aux.bytes_from_nat(List.length(U8,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,RLP.encode.many(rlps.head.child)))))
bound_bytes_from_nat
) :: Equal(Nat, 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), remember_condition, bound_child.fst)

3
base/Word/to_nat/safe.kind
View File

@ -2,4 +2,5 @@
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))
Word.to_nat.safe(size, n, H)
?to_nat.safe
//Word.to_nat.safe(size, n, H)