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

Add progress on proofs

Browse Source
This commit is contained in:
caotic123 2021-11-09 19:16:22 -03:00
parent 91e72c9581
commit 707041a334
3 changed files with 61 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
base/Ether/Bits/pad.kind
View File

@ -108,7 +108,7 @@ Ether.Bits.mul_injective(x : Nat, y : Nat, n : Nat, H : Nat.mul(Nat.succ(n), x)
}!
}!
Ether.Bits.succ_pad_nat(x : Bits) :
Ether.Bits.succ_pad_nat(x : Bits) :
Bits.to_nat(Bits.trim(Bits.length(x), x)) == Bits.to_nat(x)
case x {
e : refl

64
base/Ether/RLP/section.kind
View File

@ -19,6 +19,17 @@ Ether.RLP.Tree.to_nat(x : Ether.RLP.Tree<Bits>) : Ether.RLP.Tree<Nat>
}
Nat.complete_diff(x : Nat, y : Nat, H : Nat.lte(x, y) == true) : (x + (y - x)) == y
case x with H {
zero : refl
succ : case y with H {
zero : Empty.absurd!(Bool.false_neq_true(H))
succ :
let rec = Nat.complete_diff(x.pred, y.pred, H)
Equal.apply!!!!(Nat.succ, rec)
}!
}!
Ether.RLP.section.pad_bits8_correctude(value : Bits, H : (Ether.Bits.get_bytes_size(value) =? 1) == true) :
Bits.take(8,Ether.Bits.pad(8,value)) == Ether.Bits.pad(8,value)
let H = Ether.Bits.get_bytes_size.identity_bits_8(value, H)
@ -27,16 +38,57 @@ Ether.RLP.section.pad_bits8_correctude(value : Bits, H : (Ether.Bits.get_bytes_s
refl :
(case Nat.eql(Nat.mod(Bits.length(value),8),0) as H {
true : (_) Bits.take.identity(8, value, H)
false : (H1) ?a-70
} : (Nat.eql(Nat.mod(Bits.length(value),8),0) == H) -> Bits.take(8,H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value))) == H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value)))(refl)
false : (H1)
let H2 = Nat.Order.trichotomy(Bits.length(value), 8)
let H3 = refl :: Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value) == Bool.false(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value))
case H3 {
refl :
case H2 {
fst :
let absurd = Equal.chain(Bool, true, Nat.lte(Bits.length(value),8), false, Equal.mirror(Bool, Nat.lte(Bits.length(value),8), true, H), H2.value)
Empty.absurd!(Bool.false_neq_true(mirror(absurd)))
snd :
let H1 = Equal.rewrite(Nat, Bits.length(value), 8, H2.value, (Y) Nat.eql(Nat.mod(Y,8),0) == Bool.false, H1)
Empty.absurd!(Bool.false_neq_true(mirror(H1)))
trd :
let H2 = Nat.lte.comm.false(8, Bits.length(value), H2.value)
let H2 = Nat.mod.le_mod(Bits.length(value), 8, H2)
let H2 = Equal.mirror(Nat, Nat.mod(Bits.length(value),8), Bits.length(value), H2)
case H2 {
refl :
let H3 = Nat.complete_diff(Bits.length(value), 8, H)
let H3 = Equal.mirror(Nat, Nat.add(Bits.length(value),Nat.sub(8,Bits.length(value))), 8, H3)
let H4 = Equal.mirror(Nat, Bits.length(Bits.trim(8,value)), 8, Bits.trim.preserve_length(8, value))
let H5 = Bits.take.identity(8, Bits.trim(8,value))
let H6 = refl :: Nat.lte(8, 8) == true
let H6 = H6 :: rewrite X in Nat.lte(X, 8) == Bool.true with H4
let qed = Equal.rewrite(Nat, 8, Nat.add(Bits.length(value),Nat.sub(8,Bits.length(value))), H3, (Y) Bits.take(8,Bits.trim(Y,value)) == Bits.trim(Y,value), H5(H6))
qed
// qed :: rewrite X in Bits.take(8,Bits.trim(X,value)) == Bits.trim(X,value) with H3
} : Bits.take(8,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8, H2.b)),value)) == Bits.trim(Nat.add(Bits.length(value),Nat.sub(8, H2.b)),value)
}
}!
} : (Nat.eql(Nat.mod(Bits.length(value),8),0) == H) -> Bits.take(8,H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value))) == H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value)))(refl)
}!
Ether.RLP.section.tip_case(value : Bits, H : Bits.ltn(value,Ether.RLP.Constants.bits_128) == true) :
Ether.RLP.section.tip_case(value : Bits, H : Bits.ltn(value,Ether.RLP.Constants.bits_128) == true, H2 : (Ether.Bits.get_bytes_size(value) =? 1) == true) :
Ether.RLP.Tree.to_nat(Pair.fst(Ether.RLP.Tree(Bits),Bits,Ether.RLP.decode(Ether.Bits.pad(8,value))))
== Ether.RLP.Tree.to_nat(Ether.RLP.Tree.tip(Bits,value))
let rewr = Ether.Bits.break(8,Ether.Bits.pad(8,value)) == {Ether.Bits.pad(8,value), Bits.drop(8, Ether.Bits.pad(8,value))}
_
// ?a-46
case refl :: Ether.Bits.break(8,Ether.Bits.pad(8,value),() Pair(Ether.RLP.Tree(Bits),Bits),(byte_prefix) (rest) Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),rest),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),128),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),183),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),247),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e))))))) == Ether.RLP.decode(Ether.Bits.pad(8,value)) {
refl :
case refl :: Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),Bits.drop(8,Ether.Bits.pad(8,value))),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),128),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),183),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),247),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e)))))) == Ether.Bits.break(8,Ether.Bits.pad(8,value),() Pair(Ether.RLP.Tree(Bits),Bits),(byte_prefix) (rest) Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),rest),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),128),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),183),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),247),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e))))))) {
refl :
let pad_id = Ether.RLP.section.pad_bits8_correctude(value, H2)
let pad_id = Equal.mirror(Bits, Bits.take(8,Ether.Bits.pad(8,value)), Ether.Bits.pad(8,value), pad_id)
case pad_id {
refl : ?a
}!
}!
}!
// case Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128) {
// true : ?a
// false : _
// }!
Ether.RLP.section(tree : Ether.RLP.Tree<Bits>) :
Equal(Ether.RLP.Tree<Nat>, Ether.RLP.Tree.to_nat((Pair.fst!!(Ether.RLP.decode(Ether.RLP.encode(tree))))), Ether.RLP.Tree.to_nat(tree))

6
base/Ether/tests.kind
View File

@ -4,10 +4,8 @@ round_n(n : Nat, m : Nat) : Nat
false : round_n(n, m-8)
}
Ether.tests : Nat
let m = 32
let n = 8
m + (n - (if Nat.eql(Nat.mod(m, n), 0) then m else Nat.mod(m, n)))
Ether.tests : _
Bits.cmp.go(Bits.o(Bits.i(Bits.e)), Bits.i(Bits.e), Cmp.eql)
//let buffer = Buffer8.from_hex("d69429d7d1dd5b6f9c864d9db560d72a247c178ae86b0a")