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

prove split 0 lemma

Browse Source
This commit is contained in:
caotic123 2021-11-18 20:05:39 -03:00
parent 929b0a8a34
commit 79a3f27947
8 changed files with 107 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
base/Ether/tests.kind
View File

@ -5,7 +5,7 @@ round_n(n : Nat, m : Nat) : Nat
}
Ether.tests : _
Bits.cmp.go(Bits.o(Bits.i(Bits.e)), Bits.i(Bits.e), Cmp.eql)
Nat.to_u8(100000)
//let buffer = Buffer8.from_hex("d69429d7d1dd5b6f9c864d9db560d72a247c178ae86b0a")

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)
}!

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

@ -0,0 +1,8 @@
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)
}!

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)
}!

31
base/RLP/aux.kind
View File

@ -1,6 +1,11 @@
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(x : Nat, H : Nat.lte(x, 255) == true) : x == U8.to_nat(Nat.to_u8(x))
because_i_said_so!
// These sub-theorems were not proven yet!
// Most of them are simple, and should be finished over the next days
RLP.aux.split.0(
@ -8,20 +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)
because_i_said_so!
// let H = mirror(H)
// case H {
// refl:
// let recover_num = ?test :: List.length(U8, payload) == Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128)
// case recover_num {
// refl:
// case H {
// refl:
// List.split.length(U8, payload, tail)
// }: H.b(() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,List.nil(U8),List.concat(U8,payload,tail)), List.length(U8, payload)),Bytes.split(List.concat(U8,List.nil(U8),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)))) == Pair.new(Bytes,Bytes,payload,tail)
// }: Nat.lte( recover_num.b ,55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,List.nil(U8),List.concat(U8,payload,tail)), recover_num.b ),Bytes.split(List.concat(U8,List.nil(U8),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)))) == Pair.new(Bytes,Bytes,payload,tail)
// }: 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)
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
tail: Bytes

16
base/RLP/new_aux.kind
View File

@ -0,0 +1,16 @@
RLP.new_aux.Nat.lte.max_add(x : Nat, y : Nat, z : Nat, H : Nat.lte(Nat.succ(y), z - x) == true)
: 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 = RLP.new_aux.Nat.lte.max_add(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)
}!