mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
Add proofs on base and in Ether
This commit is contained in:
caotic123
parent
c37be43701
commit
54e40ab8e1
7
base/Bits/length/succ.kind
Normal file
7
base/Bits/length/succ.kind
Normal file
@ -0,0 +1,7 @@
|
||||
Bits.length.succ(x : Bits, n : Nat) :
|
||||
Nat.succ(Bits.length.go(x, n)) == Bits.length.go(x, Nat.succ(n))
|
||||
case x {
|
||||
e : refl
|
||||
i : Bits.length.succ(x.pred, Nat.succ(n))
|
||||
o : Bits.length.succ(x.pred, Nat.succ(n))
|
||||
}!
|
||||
34
base/Bits/take/identity.kind
Normal file
34
base/Bits/take/identity.kind
Normal file
@ -0,0 +1,34 @@
|
||||
Bits.take.identity(n : Nat, bits : Bits, H : Nat.lte(Bits.length(bits), n) == true) : Bits.take(n, bits) == bits
|
||||
case n with H {
|
||||
zero : case bits with H {
|
||||
e : refl
|
||||
i :
|
||||
let H2 = refl :: Bits.length(Bits.i(bits.pred)) == Bits.length.go(bits.pred, 1)
|
||||
let H = H :: rewrite X in Nat.lte(X,0) == Bool.true with H2
|
||||
let H = H :: rewrite X in Nat.lte(X,0) == Bool.true with mirror(Bits.length.succ(bits.pred, 0))
|
||||
let absurd = Bool.false_neq_true(H)
|
||||
Empty.absurd!(absurd)
|
||||
o :
|
||||
let H2 = refl :: Bits.length(Bits.o(bits.pred)) == Bits.length.go(bits.pred, 1)
|
||||
let H = H :: rewrite X in Nat.lte(X,0) == Bool.true with H2
|
||||
let H = H :: rewrite X in Nat.lte(X,0) == Bool.true with mirror(Bits.length.succ(bits.pred, 0))
|
||||
let absurd = Bool.false_neq_true(H)
|
||||
Empty.absurd!(absurd)
|
||||
}!
|
||||
succ :
|
||||
case bits with H {
|
||||
e : refl
|
||||
i :
|
||||
let H2 = refl :: Bits.length(Bits.i(bits.pred)) == Bits.length.go(bits.pred, 1)
|
||||
let H = Equal.rewrite(Nat, Bits.length(Bits.i(bits.pred)), Bits.length.go(bits.pred, 1), H2, (Y) Nat.lte(Y,Nat.succ(n.pred)) == Bool.true, H)
|
||||
let H = Equal.rewrite(Nat, Bits.length.go(bits.pred, 1), Nat.succ(Bits.length.go(bits.pred, 0)), Equal.mirror(Nat, Nat.succ(Bits.length.go(bits.pred, 0)), Bits.length.go(bits.pred, 1), Bits.length.succ(bits.pred, 0)), (Y) Nat.lte(Y,Nat.succ(n.pred)) == Bool.true, H)
|
||||
let rec = Bits.take.identity(n.pred, bits.pred, H)
|
||||
Equal.apply!!!!(Bits.i, rec)
|
||||
o :
|
||||
let H2 = refl :: Bits.length(Bits.o(bits.pred)) == Bits.length.go(bits.pred, 1)
|
||||
let H = Equal.rewrite(Nat, Bits.length(Bits.o(bits.pred)), Bits.length.go(bits.pred, 1), H2, (Y) Nat.lte(Y,Nat.succ(n.pred)) == Bool.true, H)
|
||||
let H = Equal.rewrite(Nat, Bits.length.go(bits.pred, 1), Nat.succ(Bits.length.go(bits.pred, 0)), Equal.mirror(Nat, Nat.succ(Bits.length.go(bits.pred, 0)), Bits.length.go(bits.pred, 1), Bits.length.succ(bits.pred, 0)), (Y) Nat.lte(Y,Nat.succ(n.pred)) == Bool.true, H)
|
||||
let rec = Bits.take.identity(n.pred, bits.pred, H)
|
||||
Equal.apply!!!!(Bits.o, rec)
|
||||
}!
|
||||
}!
|
||||
28
base/Bits/trim/preserve_length.kind
Normal file
28
base/Bits/trim/preserve_length.kind
Normal file
@ -0,0 +1,28 @@
|
||||
Bits.trim.preserve_length(n : Nat, bits : Bits) : Bits.length(Bits.trim(n, bits)) == n
|
||||
case n {
|
||||
succ : case bits {
|
||||
e :
|
||||
let rec = Bits.trim.preserve_length(n.pred, Bits.e)
|
||||
let rec = Equal.apply!!!!(Nat.succ, rec)
|
||||
let simpl = refl :: Bits.length.go(Bits.trim(n.pred,Bits.e),1) == Bits.length(Bits.trim(Nat.succ(n.pred),Bits.e))
|
||||
case simpl {
|
||||
refl :
|
||||
rec :: rewrite X in X == Nat.succ(n.pred) with Bits.length.succ(Bits.trim(n.pred,Bits.e), 0)
|
||||
}!
|
||||
o :
|
||||
let rec = Bits.trim.preserve_length(n.pred, bits.pred)
|
||||
let rec = Equal.apply!!!!(Nat.succ, rec)
|
||||
let simpl = refl :: Bits.length.go(Bits.trim(n.pred,bits.pred),1) == Bits.length(Bits.trim(Nat.succ(n.pred), Bits.o(bits.pred)))
|
||||
case simpl {
|
||||
refl : rec :: rewrite X in X == Nat.succ(n.pred) with Bits.length.succ(Bits.trim(n.pred, bits.pred), 0)
|
||||
}!
|
||||
i :
|
||||
let rec = Bits.trim.preserve_length(n.pred, bits.pred)
|
||||
let rec = Equal.apply!!!!(Nat.succ, rec)
|
||||
let simpl = refl :: Bits.length.go(Bits.trim(n.pred,bits.pred),1) == Bits.length(Bits.trim(Nat.succ(n.pred), Bits.i(bits.pred)))
|
||||
case simpl {
|
||||
refl : rec :: rewrite X in X == Nat.succ(n.pred) with Bits.length.succ(Bits.trim(n.pred, bits.pred), 0)
|
||||
}!
|
||||
}!
|
||||
zero : refl
|
||||
}!
|
||||
@ -1,3 +1,87 @@
|
||||
Ether.Bits.get_bytes_size(bytes : Bits) : Nat
|
||||
let bytes_size = Bits.length(bytes) / 8
|
||||
if (Nat.mod(Bits.length(bytes), 8)) >? 0 then bytes_size +1 else Nat.max(1, bytes_size)
|
||||
if (Nat.mod(Bits.length(bytes), 8)) >? 0 then bytes_size +1 else Nat.max(1, bytes_size)
|
||||
|
||||
Nat.gte.zero_right(n: Nat, Hyp: Nat.gtn(n, 0) == false): n == 0
|
||||
case n with Hyp {
|
||||
zero : refl
|
||||
succ : Empty.absurd!(Bool.false_neq_true(mirror(Hyp)))
|
||||
}!
|
||||
|
||||
Ether.Bits.get_bytes_size.identity_bits_8(bytes : Bits) :
|
||||
((Ether.Bits.get_bytes_size(bytes) =? 1) == true) -> Nat.lte(Bits.length(bytes), 8) == true
|
||||
let remember = case Nat.gtn(Nat.mod(Bits.length(bytes),8), 0) {
|
||||
true : (H)
|
||||
let H = mirror(H)
|
||||
case H {
|
||||
refl :
|
||||
let H3 = refl :: Bool.true(() Nat,Nat.add(Nat.div(Bits.length(bytes),8),1),Nat.max(1,Nat.div(Bits.length(bytes),8))) == Nat.add(Nat.div(Bits.length(bytes),8),1)
|
||||
let H3 = Equal.mirror(Nat, Bool.true(() Nat,Nat.add(Nat.div(Bits.length(bytes),8),1),Nat.max(1,Nat.div(Bits.length(bytes),8))), Nat.add(Nat.div(Bits.length(bytes),8),1), H3)
|
||||
case H3 {
|
||||
refl :
|
||||
let remember = case (Nat.div(Bits.length(bytes),8)) as s {
|
||||
zero : (H4, H5)
|
||||
let H5 = Nat.div_mod.recover(Bits.length(bytes), 8, refl)
|
||||
let H5 = H5 :: rewrite Y in Nat.add(Nat.mod(Bits.length(bytes),8),Nat.mul(Y,8)) == Bits.length(bytes) with H4
|
||||
let H5 = (H5 :: rewrite Y in Y == Bits.length(bytes) with Nat.add.comm(Nat.mod(Bits.length(bytes),8), 0)) :: Nat.mod(Bits.length(bytes),8) == Bits.length(bytes)
|
||||
let H6 = Nat.lte.comm.false(8, Nat.mod(Bits.length(bytes),8), Nat.mod.small(Bits.length(bytes), 8, refl))
|
||||
let H6 = Nat.lte.succ_left(Nat.mod(Bits.length(bytes),8), 8, H6)
|
||||
let H6 = H6 :: rewrite Y in Nat.lte(Y,8) == Bool.true with H5
|
||||
H6
|
||||
succ : (H4, H5)
|
||||
let H6 = Nat.div_mod.recover(Bits.length(bytes), 8, refl)
|
||||
let H7 = Nat.eql.reflexivity(Nat.add(Nat.div(Bits.length(bytes),8),1), 1, H5)
|
||||
let H7 = H7 :: rewrite X in X == _ with Nat.add.comm(Nat.div(Bits.length(bytes),8), 1)
|
||||
let H7 = Nat.succ_inj!!(H7 :: Nat.succ(Nat.div(Bits.length(bytes),8)) == 1)
|
||||
let H4 = mirror(H4) :: rewrite Y in _ == Y with H7
|
||||
Empty.absurd!(Nat.succ_neq_zero!(H4))
|
||||
} : (Nat.div(Bits.length(bytes),8) == s) -> (:Nat.eql(Nat.add(Nat.div(Bits.length(bytes),8),1),1) == Bool.true) -> Nat.lte(Bits.length(bytes),8) == Bool.true
|
||||
remember(refl)
|
||||
}!
|
||||
} : (:Nat.eql(H.b(() Nat,Nat.add(Nat.div(Bits.length(bytes),8),1),Nat.max(1,Nat.div(Bits.length(bytes),8))),1) == Bool.true) -> Nat.lte(Bits.length(bytes),8) == Bool.true
|
||||
false :
|
||||
(H, H2)
|
||||
let H_lte = Nat.gte.zero_right(Nat.mod(Bits.length(bytes),8), H)
|
||||
case Nat.gtn(Nat.mod(Bits.length(bytes),8), 0) with H2 {
|
||||
true :
|
||||
def H2 = H2 :: Nat.eql(Nat.add(Nat.div(Bits.length(bytes),8),1),1) == Bool.true
|
||||
def H2 = Equal.rewrite(Nat, Nat.add(Nat.div(Bits.length(bytes),8),1), Nat.add(1,Nat.div(Bits.length(bytes),8)), Nat.add.comm(Nat.div(Bits.length(bytes),8), 1),
|
||||
(Y) Nat.eql(Y,1) == Bool.true, H2)
|
||||
let H2 = Nat.eql.reflexivity(Nat.div(Bits.length(bytes),8), 0, H2 :: Nat.eql(Nat.div(Bits.length(bytes),8),0) == Bool.true)
|
||||
let H3 = Nat.div_mod.recover(Bits.length(bytes), 8, refl)
|
||||
let H3 = H3 :: rewrite Y in
|
||||
Nat.add(Y,Nat.mul(Nat.div(Bits.length(bytes),8),8)) == Bits.length(bytes) with H_lte
|
||||
let H3 = H3 :: rewrite Y in
|
||||
Nat.add(0,Nat.mul(Y,8)) == Bits.length(bytes) with H2
|
||||
let H3 = H3 :: 0 == Bits.length(bytes)
|
||||
refl :: rewrite Y in Nat.lte(Y,8) == Bool.true with H3
|
||||
false :
|
||||
let H2 = H2 :: Nat.eql(Nat.max(1,Nat.div(Bits.length(bytes),8)),1) == Bool.true
|
||||
let H2 = Nat.eql.reflexivity(Nat.max(1,Nat.div(Bits.length(bytes),8)), 1, H2)
|
||||
let H2 = Nat.max.less!!(H2)
|
||||
(case Nat.div(Bits.length(bytes),8) {
|
||||
zero : (dec)
|
||||
let H3 = Nat.div_mod.recover(Bits.length(bytes), 8, refl)
|
||||
let H3 = H3 :: rewrite Y in Nat.add(Nat.mod(Bits.length(bytes),8),Nat.mul(Y,8)) == Bits.length(bytes) with dec
|
||||
let H3 = H3 :: rewrite Y in Nat.add(Y,Nat.mul(0,8)) == Bits.length(bytes) with H_lte
|
||||
let H3 = H3 :: 0 == Bits.length(bytes)
|
||||
refl :: rewrite X in Nat.lte(X,8) == Bool.true with H3
|
||||
succ : (dec) (case self.pred as dec_number {
|
||||
zero : (dec_number)
|
||||
let dec = dec :: rewrite X in Nat.div(Bits.length(bytes),8) == Nat.succ(X) with dec_number
|
||||
let H3 = Nat.div_mod.recover(Bits.length(bytes), 8, refl)
|
||||
let H3 = H3 :: rewrite Y in Nat.add(Nat.mod(Bits.length(bytes),8),Nat.mul(Y,8)) == Bits.length(bytes) with dec
|
||||
let H3 = H3 :: rewrite Y in Nat.add(Y,Nat.mul(1,8)) == Bits.length(bytes) with H_lte
|
||||
let H3 = H3 :: 8 == Bits.length(bytes)
|
||||
refl :: rewrite X in Nat.lte(X,8) == Bool.true with H3
|
||||
succ : (dec_number)
|
||||
let dec = dec :: rewrite X in Nat.div(Bits.length(bytes),8) == Nat.succ(X) with dec_number
|
||||
let H2 = H2 :: rewrite X in Nat.lte(X,1) == Bool.true with dec
|
||||
Empty.absurd!(Bool.false_neq_true(H2))
|
||||
} : (self.pred == dec_number) -> _)(refl)
|
||||
|
||||
} : (Nat.div(Bits.length(bytes),8) == self) -> Nat.lte(Bits.length(bytes),8) == Bool.true)(refl)
|
||||
}!
|
||||
} : (Nat.gtn(Nat.mod(Bits.length(bytes),8), 0) == self) -> (:Nat.eql(Nat.gtn(Nat.mod(Bits.length(bytes),8),0,() Nat,Nat.add(Nat.div(Bits.length(bytes),8),1),Nat.max(1,Nat.div(Bits.length(bytes),8))),1) == Bool.true) -> Nat.lte(Bits.length(bytes),8) == Bool.true
|
||||
remember(refl)
|
||||
|
||||
|
||||
213
base/Ether/Bits/pad.kind
Normal file
213
base/Ether/Bits/pad.kind
Normal file
@ -0,0 +1,213 @@
|
||||
Ether.Bits.pad(n : Nat bits : Bits) : Bits
|
||||
let size = Bits.length(bits)
|
||||
if Nat.eql(Nat.mod(size, n), 0) then
|
||||
bits
|
||||
else
|
||||
Bits.trim(size + (n - (Nat.mod(size, n))), bits)
|
||||
|
||||
Ether.Bits.add_round_is_multiple(n : Nat, bits : Bits)
|
||||
: Nat.mod(Bits.length(Ether.Bits.pad(n, bits)), n) == 0
|
||||
let norm = refl :: Nat.eql(Nat.mod(Bits.length(bits),n),0,() Bits,bits,Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits)) == Ether.Bits.pad(n, bits)
|
||||
case norm {
|
||||
refl : (case Nat.eql(Nat.mod(Bits.length(bits),n),0) {
|
||||
true : (H)
|
||||
let H = Equal.mirror(Bool, Nat.eql(Nat.mod(Bits.length(bits),n),0), true, H)
|
||||
case H {
|
||||
refl :
|
||||
let H = Nat.eql.reflexivity(Nat.mod(Bits.length(bits),n), 0, mirror(H))
|
||||
let norm = refl ::
|
||||
bits == Bool.true(() Bits,bits,Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits))
|
||||
case norm {
|
||||
refl : H
|
||||
}!
|
||||
} : Nat.mod(Bits.length(H.b(() Bits,bits,Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits))),n) == 0
|
||||
false : (H)
|
||||
let H = Equal.mirror(Bool, Nat.eql(Nat.mod(Bits.length(bits),n),0), false, H)
|
||||
case H {
|
||||
refl :
|
||||
let norm = refl :: Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits) == Bool.false(() Bits,bits,Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits))
|
||||
case norm {
|
||||
refl :
|
||||
def H = Bits.trim.preserve_length(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))), bits)
|
||||
def H = Equal.mirror(Nat, Bits.length(Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits)), Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))), H)
|
||||
case H {
|
||||
refl :
|
||||
let H = Nat.div_mod.recover(Bits.length(bits), n)
|
||||
_ // (m + (n - (m % n))) % n = 0
|
||||
|
||||
} : Nat.mod(H.b, n) == 0
|
||||
}!
|
||||
} : Nat.mod(Bits.length(H.b(() Bits,bits,Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits))),n) == 0
|
||||
} : (Nat.eql(Nat.mod(Bits.length(bits),n),0) == self) -> _)(refl)
|
||||
}!
|
||||
|
||||
Ether.Bits.add_self_absurd(x : Nat, n: Nat) : Equal(Nat, Nat.add(n, Nat.succ(x)), n) -> Empty
|
||||
case n {
|
||||
succ :
|
||||
(H)
|
||||
let H = Nat.succ_inj!!(H)
|
||||
let qed = Ether.Bits.add_self_absurd(x, n.pred, H)
|
||||
qed
|
||||
zero : (H) Nat.succ_neq_zero!(H)
|
||||
}!
|
||||
|
||||
Ether.Bits.add_injective(x : Nat, y : Nat, n : Nat, H : Nat.add(Nat.succ(n), x) == Nat.add(Nat.succ(n), y)) : x == y
|
||||
case x with H {
|
||||
succ : case y with H {
|
||||
succ :
|
||||
let com_H = Nat.add.comm(Nat.succ(n), Nat.succ(x.pred))
|
||||
let com_H2 = Nat.add.comm(Nat.succ(n), Nat.succ(y.pred))
|
||||
let H_rewrite = H :: rewrite Y in Y == _ with com_H
|
||||
let H_rewrite = H_rewrite :: rewrite Y in _ == Y with com_H2
|
||||
let H_rewrite_inj = Nat.succ_inj!!(H_rewrite)
|
||||
let H_rewrite_inj = H_rewrite_inj :: rewrite Y in Y == _ with Nat.add.comm(x.pred, Nat.succ(n))
|
||||
let H_rewrite_inj = H_rewrite_inj :: rewrite Y in _ == Y with Nat.add.comm(y.pred, Nat.succ(n))
|
||||
let H2 = Ether.Bits.add_injective(x.pred, y.pred, n, H_rewrite_inj)
|
||||
Equal.apply!!!!(Nat.succ, H2)
|
||||
zero :
|
||||
let rewrite_0_com =
|
||||
Nat.add.comm(Nat.succ(n), 0)
|
||||
let H = H :: rewrite Y in _ == Y with rewrite_0_com
|
||||
let absurd = Ether.Bits.add_self_absurd!!(H)
|
||||
Empty.absurd!(absurd)
|
||||
}!
|
||||
zero : case y with H {
|
||||
succ :
|
||||
let H = mirror(H)
|
||||
let rewrite_0_com = Nat.add.comm(Nat.succ(n), 0)
|
||||
let H = H :: rewrite Y in _ == Y with rewrite_0_com
|
||||
let absurd = Ether.Bits.add_self_absurd!!(H)
|
||||
Empty.absurd!(absurd)
|
||||
zero : refl
|
||||
}!
|
||||
}!
|
||||
|
||||
|
||||
Ether.Bits.mul_injective(x : Nat, y : Nat, n : Nat, H : Nat.mul(Nat.succ(n), x) == Nat.mul(Nat.succ(n), y)) : x == y
|
||||
case x with H {
|
||||
succ : case y with H {
|
||||
succ :
|
||||
|
||||
let H = H :: rewrite Y in Y == _ with Nat.mul.succ_right(Nat.succ(n), x.pred)
|
||||
let H = H :: rewrite Y in _ == Y with Nat.mul.succ_right(Nat.succ(n), y.pred)
|
||||
let inj_add = Ether.Bits.add_injective(Nat.mul(Nat.succ(n), x.pred), Nat.mul(Nat.succ(n), y.pred), n, H)
|
||||
let H = Ether.Bits.mul_injective(x.pred, y.pred, n, inj_add)
|
||||
Equal.apply!!!!(Nat.succ, H)
|
||||
zero :
|
||||
let H = H :: rewrite Y in _ == Y with Nat.mul.comm(Nat.succ(n), 0)
|
||||
let H4 = Nat.succ_neq_zero!(H)
|
||||
Empty.absurd!(H4)
|
||||
}!
|
||||
zero : case y with H {
|
||||
succ :
|
||||
let H = H :: rewrite Y in Y == _ with Nat.mul.comm(Nat.succ(n), 0)
|
||||
let H4 = Nat.succ_neq_zero!(mirror(H))
|
||||
Empty.absurd!(H4)
|
||||
zero :
|
||||
refl
|
||||
}!
|
||||
}!
|
||||
|
||||
Ether.Bits.succ_pad_nat(x : Bits) :
|
||||
Bits.to_nat(Bits.trim(Bits.length(x), x)) == Bits.to_nat(x)
|
||||
case x {
|
||||
e : refl
|
||||
o :
|
||||
let remove_tail_rec = Bits.length.succ(x.pred, 0)
|
||||
let refl_cont =
|
||||
refl ::
|
||||
Bits.length.go(x.pred, 1) == Bits.length(Bits.o(x.pred))
|
||||
case refl_cont {
|
||||
refl :
|
||||
case remove_tail_rec {
|
||||
refl :
|
||||
let rec = Ether.Bits.succ_pad_nat(x.pred)
|
||||
let rec = Equal.apply!!!!(Nat.mul(2), rec)
|
||||
rec
|
||||
}!
|
||||
}!
|
||||
i :
|
||||
let remove_tail_rec = Bits.length.succ(x.pred, 0)
|
||||
let refl_cont =
|
||||
refl ::
|
||||
Bits.length.go(x.pred, 1) == Bits.length(Bits.i(x.pred))
|
||||
case refl_cont {
|
||||
refl :
|
||||
case remove_tail_rec {
|
||||
refl :
|
||||
let rec = Ether.Bits.succ_pad_nat(x.pred)
|
||||
let rec = Equal.apply!!!!(Nat.mul(2), rec)
|
||||
Equal.apply(Nat, Nat, Nat.mul(2,Bits.to_nat(Bits.trim(Bits.length.go(x.pred,0),x.pred))),
|
||||
Nat.mul(2,Bits.to_nat(x.pred)), Nat.succ, rec)
|
||||
}!
|
||||
}!
|
||||
}!
|
||||
|
||||
Ether.Bits.nat_succ_pad_nat(y : Nat, x : Bits, H :
|
||||
Bits.to_nat(Bits.trim(y, x)) == Bits.to_nat(x)) :
|
||||
Bits.to_nat(Bits.trim(Nat.succ(y), x)) == Bits.to_nat(x)
|
||||
case y with H {
|
||||
zero :
|
||||
case x with H {
|
||||
i :
|
||||
let H = H :: 0 == Nat.succ(Nat.mul(2, Bits.to_nat(x.pred)))
|
||||
let absurd = Nat.succ_neq_zero!(mirror(H))
|
||||
Empty.absurd!(absurd)
|
||||
o :
|
||||
let H = H :: 0 == Nat.mul(2, Bits.to_nat(x.pred))
|
||||
H
|
||||
e : refl
|
||||
}!
|
||||
succ : case x with H {
|
||||
i :
|
||||
let H = H :: Nat.succ(Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,x.pred)))) == Nat.succ(Nat.mul(2, Bits.to_nat(x.pred)))
|
||||
let H = Nat.succ_inj(Nat.mul(2,Bits.to_nat(Bits.trim(y.pred,x.pred))), Nat.mul(2,Bits.to_nat(x.pred)), H)
|
||||
let H = Ether.Bits.mul_injective(Bits.to_nat(Bits.trim(y.pred,x.pred)), Bits.to_nat(x.pred), 1, H)
|
||||
let H2 = Ether.Bits.nat_succ_pad_nat(y.pred, x.pred, H)
|
||||
let qed = Equal.apply!!!!(Nat.succ . Nat.mul(2), H2)
|
||||
qed
|
||||
o :
|
||||
let H = H :: Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,x.pred))) == Nat.mul(2, Bits.to_nat(x.pred))
|
||||
let H = Ether.Bits.mul_injective(Bits.to_nat(Bits.trim(y.pred,x.pred)), Bits.to_nat(x.pred), 1, H)
|
||||
let H2 = Ether.Bits.nat_succ_pad_nat(y.pred, x.pred, H)
|
||||
let qed = Equal.apply!!!!(Nat.mul(2), H2)
|
||||
qed
|
||||
e :
|
||||
let H = H :: Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,Bits.e))) == Nat.mul(2, 0)
|
||||
let absurd_mul_injective = Ether.Bits.mul_injective(Bits.to_nat(Bits.trim(y.pred,Bits.e)), 0, 1, H)
|
||||
let H2 = Ether.Bits.nat_succ_pad_nat(y.pred, Bits.e, absurd_mul_injective)
|
||||
let qed = Equal.apply!!!!(Nat.mul(2), H2)
|
||||
qed
|
||||
}!
|
||||
}!
|
||||
|
||||
Ether.Bits.pad_nat(x : Bits, y : Nat) :
|
||||
Bits.to_nat(Bits.trim(Nat.add(y, Bits.length(x)), x)) == Bits.to_nat(x)
|
||||
case y {
|
||||
succ :
|
||||
let H = Ether.Bits.pad_nat(x, y.pred)
|
||||
Ether.Bits.nat_succ_pad_nat!!(H)
|
||||
zero : Ether.Bits.succ_pad_nat(x)
|
||||
}!
|
||||
|
||||
Ether.Bits.pad_bytes_identity(n : Nat, bits : Bits) : Bits.to_nat(Ether.Bits.pad(n, bits)) == Bits.to_nat(bits)
|
||||
let simpl = refl ::
|
||||
(Nat.eql(Nat.mod(Bits.length(bits),n),0,() Bits,bits,Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits)) == Ether.Bits.pad(n, bits))
|
||||
case simpl {
|
||||
refl : case Nat.eql(Nat.mod(Bits.length(bits),n),0) {
|
||||
true :
|
||||
refl
|
||||
false :
|
||||
let simpl = refl :: Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits) == Bool.false(() Bits,bits,Bits.trim(Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))),bits))
|
||||
case simpl {
|
||||
refl :
|
||||
let H = Ether.Bits.pad_nat(bits, Nat.sub(n,Nat.mod(Bits.length(bits),n)))
|
||||
let H1 = Nat.add.comm(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n)))
|
||||
let H1 = Equal.mirror(Nat, Nat.add(Bits.length(bits),Nat.sub(n,Nat.mod(Bits.length(bits),n))), Nat.add(Nat.sub(n,Nat.mod(Bits.length(bits),n)),Bits.length(bits)), H1)
|
||||
case H1 {
|
||||
refl : Ether.Bits.pad_nat(bits, Nat.sub(n,Nat.mod(Bits.length(bits),n)))
|
||||
} : Bits.to_nat(Bits.trim(H1.b, bits)) == Bits.to_nat(bits)
|
||||
}!
|
||||
}!
|
||||
}!
|
||||
|
||||
@ -1,4 +1,5 @@
|
||||
type Ether.RLP.Tree {
|
||||
tip(value : Bits)
|
||||
list(value : List<Ether.RLP.Tree>)
|
||||
//changed to become a functor
|
||||
type Ether.RLP.Tree<A : Type> {
|
||||
tip(value : A)
|
||||
list(value : List<Ether.RLP.Tree<A>>)
|
||||
}
|
||||
@ -1,7 +1,7 @@
|
||||
Ether.Bits.break(len : Nat, bits : Bits) : Pair<Bits, Bits>
|
||||
{Bits.take(len, bits), Bits.drop(len, bits)}
|
||||
|
||||
Ether.RLP.decode.decode_list(value : Bits) : Pair<List<Ether.RLP.Tree>, Bits>
|
||||
Ether.RLP.decode.decode_list(value : Bits) : Pair<List<Ether.RLP.Tree<Bits>>, Bits>
|
||||
if (Bits.eql(value, Bits.e)) then
|
||||
{[], value}
|
||||
else
|
||||
@ -9,29 +9,29 @@ Ether.RLP.decode.decode_list(value : Bits) : Pair<List<Ether.RLP.Tree>, Bits>
|
||||
let {trees, rest} = Ether.RLP.decode.decode_list(rest)
|
||||
{tree & trees, rest}
|
||||
|
||||
Ether.RLP.decode(bits : Bits) : Pair<Ether.RLP.Tree, Bits>
|
||||
Ether.RLP.decode(bits : Bits) : Pair<Ether.RLP.Tree<Bits>, Bits>
|
||||
let {byte_prefix, rest} = Ether.Bits.break(8, bits)
|
||||
switch (Bits.ltn(byte_prefix)) {
|
||||
Ether.RLP.Constants.bits_128 :
|
||||
{Ether.RLP.Tree.tip(bits), rest}
|
||||
{Ether.RLP.Tree.tip!(bits), rest}
|
||||
Ether.RLP.Constants.bits_184 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 128) * 8
|
||||
let {prefix, rest} = Ether.Bits.break(content_length, rest)
|
||||
{Ether.RLP.Tree.tip(prefix), rest}
|
||||
{Ether.RLP.Tree.tip!(prefix), rest}
|
||||
Ether.RLP.Constants.bits_192 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 183) * 8
|
||||
let {head, rest} = Ether.Bits.break(content_length, rest)
|
||||
let length = Ether.RLP.encode.read.binary(head)
|
||||
let {prefix, rest} = Ether.Bits.break(length*8, rest)
|
||||
{Ether.RLP.Tree.tip(prefix), rest}
|
||||
{Ether.RLP.Tree.tip!(prefix), rest}
|
||||
Ether.RLP.Constants.bits_248 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 192) * 8
|
||||
let {xs, rest} = Ether.RLP.decode.decode_list(rest)
|
||||
{Ether.RLP.Tree.list(xs), rest}
|
||||
{Ether.RLP.Tree.list!(xs), rest}
|
||||
Ether.RLP.Constants.bits_255 :
|
||||
let content_length = (Bits.to_nat(byte_prefix) - 247) * 8
|
||||
let {head, rest} = Ether.Bits.break(content_length, rest)
|
||||
let length = Ether.RLP.encode.read.binary(head)
|
||||
let {xs, rest} = Ether.RLP.decode.decode_list(rest)
|
||||
{Ether.RLP.Tree.list(xs), rest}
|
||||
} default {Ether.RLP.Tree.tip(Bits.e), Bits.e}
|
||||
{Ether.RLP.Tree.list!(xs), rest}
|
||||
} default {Ether.RLP.Tree.tip!(Bits.e), Bits.e}
|
||||
@ -1,181 +1,12 @@
|
||||
Ether.RLP.pad_bytes(bits : Bits) : Bits
|
||||
let size = Bits.length(bits)
|
||||
Bits.trim(((8 * ((size + 7) / 8)) - size) + size, bits)
|
||||
|
||||
Ether.RLP.pad_8bits(bits : Bits) : Bits
|
||||
let size = Bits.length(bits)
|
||||
Bits.trim(8, bits)
|
||||
|
||||
Bits.size.rec(x : Bits, n : Nat) :
|
||||
Nat.succ(Bits.length.go(x, n)) == Bits.length.go(x, Nat.succ(n))
|
||||
case x {
|
||||
e : refl
|
||||
i : Bits.size.rec(x.pred, Nat.succ(n))
|
||||
o : Bits.size.rec(x.pred, Nat.succ(n))
|
||||
}!
|
||||
|
||||
Ether.RLP.add_self_absurd(x : Nat, n: Nat) : Equal(Nat, Nat.add(n, Nat.succ(x)), n) -> Empty
|
||||
case n {
|
||||
succ :
|
||||
(H)
|
||||
let H = Nat.succ_inj!!(H)
|
||||
let qed = Ether.RLP.add_self_absurd(x, n.pred, H)
|
||||
qed
|
||||
zero : (H) Nat.succ_neq_zero!(H)
|
||||
}!
|
||||
|
||||
Ether.RLP.add_injective(x : Nat, y : Nat, n : Nat, H : Nat.add(Nat.succ(n), x) == Nat.add(Nat.succ(n), y)) : x == y
|
||||
case x with H {
|
||||
succ : case y with H {
|
||||
succ :
|
||||
let com_H = Nat.add.comm(Nat.succ(n), Nat.succ(x.pred))
|
||||
let com_H2 = Nat.add.comm(Nat.succ(n), Nat.succ(y.pred))
|
||||
let H_rewrite = H :: rewrite Y in Y == _ with com_H
|
||||
let H_rewrite = H_rewrite :: rewrite Y in _ == Y with com_H2
|
||||
let H_rewrite_inj = Nat.succ_inj!!(H_rewrite)
|
||||
let H_rewrite_inj = H_rewrite_inj :: rewrite Y in Y == _ with Nat.add.comm(x.pred, Nat.succ(n))
|
||||
let H_rewrite_inj = H_rewrite_inj :: rewrite Y in _ == Y with Nat.add.comm(y.pred, Nat.succ(n))
|
||||
let H2 = Ether.RLP.add_injective(x.pred, y.pred, n, H_rewrite_inj)
|
||||
Equal.apply!!!!(Nat.succ, H2)
|
||||
zero :
|
||||
let rewrite_0_com =
|
||||
Nat.add.comm(Nat.succ(n), 0)
|
||||
let H = H :: rewrite Y in _ == Y with rewrite_0_com
|
||||
let absurd = Ether.RLP.add_self_absurd!!(H)
|
||||
Empty.absurd!(absurd)
|
||||
}!
|
||||
zero : case y with H {
|
||||
succ :
|
||||
let H = mirror(H)
|
||||
let rewrite_0_com = Nat.add.comm(Nat.succ(n), 0)
|
||||
let H = H :: rewrite Y in _ == Y with rewrite_0_com
|
||||
let absurd = Ether.RLP.add_self_absurd!!(H)
|
||||
Empty.absurd!(absurd)
|
||||
zero : refl
|
||||
}!
|
||||
}!
|
||||
|
||||
Ether.RLP.mul_injective(x : Nat, y : Nat, n : Nat, H : Nat.mul(Nat.succ(n), x) == Nat.mul(Nat.succ(n), y)) : x == y
|
||||
case x with H {
|
||||
succ : case y with H {
|
||||
succ :
|
||||
|
||||
let H = H :: rewrite Y in Y == _ with Nat.mul.succ_right(Nat.succ(n), x.pred)
|
||||
let H = H :: rewrite Y in _ == Y with Nat.mul.succ_right(Nat.succ(n), y.pred)
|
||||
let inj_add = Ether.RLP.add_injective(Nat.mul(Nat.succ(n), x.pred), Nat.mul(Nat.succ(n), y.pred), n, H)
|
||||
let H = Ether.RLP.mul_injective(x.pred, y.pred, n, inj_add)
|
||||
Equal.apply!!!!(Nat.succ, H)
|
||||
zero :
|
||||
let H = H :: rewrite Y in _ == Y with Nat.mul.comm(Nat.succ(n), 0)
|
||||
let H4 = Nat.succ_neq_zero!(H)
|
||||
Empty.absurd!(H4)
|
||||
}!
|
||||
zero : case y with H {
|
||||
succ :
|
||||
let H = H :: rewrite Y in Y == _ with Nat.mul.comm(Nat.succ(n), 0)
|
||||
let H4 = Nat.succ_neq_zero!(mirror(H))
|
||||
Empty.absurd!(H4)
|
||||
zero :
|
||||
refl
|
||||
}!
|
||||
}!
|
||||
|
||||
Ether.RLP.succ_pad_nat(x : Bits) :
|
||||
Bits.to_nat(Bits.trim(Bits.length(x), x)) == Bits.to_nat(x)
|
||||
case x {
|
||||
e : refl
|
||||
o :
|
||||
let remove_tail_rec = Bits.size.rec(x.pred, 0)
|
||||
let refl_cont =
|
||||
refl ::
|
||||
Bits.length.go(x.pred, 1) == Bits.length(Bits.o(x.pred))
|
||||
case refl_cont {
|
||||
refl :
|
||||
case remove_tail_rec {
|
||||
refl :
|
||||
let rec = Ether.RLP.succ_pad_nat(x.pred)
|
||||
let rec = Equal.apply!!!!(Nat.mul(2), rec)
|
||||
rec
|
||||
}!
|
||||
}!
|
||||
i :
|
||||
let remove_tail_rec = Bits.size.rec(x.pred, 0)
|
||||
let refl_cont =
|
||||
refl ::
|
||||
Bits.length.go(x.pred, 1) == Bits.length(Bits.i(x.pred))
|
||||
case refl_cont {
|
||||
refl :
|
||||
case remove_tail_rec {
|
||||
refl :
|
||||
let rec = Ether.RLP.succ_pad_nat(x.pred)
|
||||
let rec = Equal.apply!!!!(Nat.mul(2), rec)
|
||||
Equal.apply(Nat, Nat, Nat.mul(2,Bits.to_nat(Bits.trim(Bits.length.go(x.pred,0),x.pred))),
|
||||
Nat.mul(2,Bits.to_nat(x.pred)), Nat.succ, rec)
|
||||
}!
|
||||
}!
|
||||
}!
|
||||
|
||||
Ether.RLP.nat_succ_pad_nat(y : Nat, x : Bits, H :
|
||||
Bits.to_nat(Bits.trim(y, x)) == Bits.to_nat(x)) :
|
||||
Bits.to_nat(Bits.trim(Nat.succ(y), x)) == Bits.to_nat(x)
|
||||
case y with H {
|
||||
zero :
|
||||
case x with H {
|
||||
i :
|
||||
let H = H :: 0 == Nat.succ(Nat.mul(2, Bits.to_nat(x.pred)))
|
||||
let absurd = Nat.succ_neq_zero!(mirror(H))
|
||||
Empty.absurd!(absurd)
|
||||
o :
|
||||
let H = H :: 0 == Nat.mul(2, Bits.to_nat(x.pred))
|
||||
H
|
||||
e : refl
|
||||
}!
|
||||
succ : case x with H {
|
||||
i :
|
||||
let H = H :: Nat.succ(Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,x.pred)))) == Nat.succ(Nat.mul(2, Bits.to_nat(x.pred)))
|
||||
let H = Nat.succ_inj(Nat.mul(2,Bits.to_nat(Bits.trim(y.pred,x.pred))), Nat.mul(2,Bits.to_nat(x.pred)), H)
|
||||
let H = Ether.RLP.mul_injective(Bits.to_nat(Bits.trim(y.pred,x.pred)), Bits.to_nat(x.pred), 1, H)
|
||||
let H2 = Ether.RLP.nat_succ_pad_nat(y.pred, x.pred, H)
|
||||
let qed = Equal.apply!!!!(Nat.succ . Nat.mul(2), H2)
|
||||
qed
|
||||
o :
|
||||
let H = H :: Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,x.pred))) == Nat.mul(2, Bits.to_nat(x.pred))
|
||||
let H = Ether.RLP.mul_injective(Bits.to_nat(Bits.trim(y.pred,x.pred)), Bits.to_nat(x.pred), 1, H)
|
||||
let H2 = Ether.RLP.nat_succ_pad_nat(y.pred, x.pred, H)
|
||||
let qed = Equal.apply!!!!(Nat.mul(2), H2)
|
||||
qed
|
||||
e :
|
||||
let H = H :: Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,Bits.e))) == Nat.mul(2, 0)
|
||||
let absurd_mul_injective = Ether.RLP.mul_injective(Bits.to_nat(Bits.trim(y.pred,Bits.e)), 0, 1, H)
|
||||
let H2 = Ether.RLP.nat_succ_pad_nat(y.pred, Bits.e, absurd_mul_injective)
|
||||
let qed = Equal.apply!!!!(Nat.mul(2), H2)
|
||||
qed
|
||||
}!
|
||||
}!
|
||||
|
||||
Ether.RLP.pad_nat(x : Bits, y : Nat) :
|
||||
Bits.to_nat(Bits.trim(Nat.add(y, Bits.length(x)), x)) == Bits.to_nat(x)
|
||||
case y {
|
||||
succ :
|
||||
let H = Ether.RLP.pad_nat(x, y.pred)
|
||||
Ether.RLP.nat_succ_pad_nat!!(H)
|
||||
zero : Ether.RLP.succ_pad_nat(x)
|
||||
}!
|
||||
|
||||
Ether.RLP.pad_bytes_identity(bits : Bits) :
|
||||
Bits.to_nat(Ether.RLP.pad_bytes(bits)) == Bits.to_nat(bits)
|
||||
Ether.RLP.pad_nat(bits, Nat.sub(Nat.mul(8,Nat.div(Nat.add(Bits.length(bits),7),8)),
|
||||
Bits.length(bits)))
|
||||
|
||||
Ether.RLP.encode(tree : Ether.RLP.Tree) : Bits
|
||||
Ether.RLP.encode(tree : Ether.RLP.Tree<Bits>) : Bits
|
||||
case tree {
|
||||
tip :
|
||||
let bytes_size = Ether.Bits.get_bytes_size(tree.value)
|
||||
// let u16_char = Bits.trim(4, tree.value)
|
||||
if (bytes_size =? 1) && Bits.ltn(tree.value, Ether.RLP.Constants.bits_128) then
|
||||
Ether.RLP.pad_bytes(tree.value)
|
||||
Ether.Bits.pad(8, tree.value)
|
||||
else
|
||||
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 128), Ether.RLP.pad_bytes(tree.value))
|
||||
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 128), Ether.Bits.pad(8, tree.value))
|
||||
list :
|
||||
let bytes = Bits.e
|
||||
for item in tree.value with bytes :
|
||||
@ -187,12 +18,12 @@ Ether.RLP.encode(tree : Ether.RLP.Tree) : Bits
|
||||
Ether.RPL.proof.encode_length(value : Nat, offSet : Nat) : Bits
|
||||
switch(Nat.ltn(value)) {
|
||||
56 :
|
||||
Ether.RLP.pad_8bits(Nat.to_bits(value + offSet))
|
||||
Ether.Bits.pad(8, Nat.to_bits(value + offSet))
|
||||
}
|
||||
default
|
||||
let binary_encoding = Ether.RPL.proof.encode.binary(value)
|
||||
let len = Ether.Bits.get_bytes_size(binary_encoding)
|
||||
let len = Ether.RLP.pad_8bits(Nat.to_bits(len + offSet + 55))
|
||||
let len = Ether.Bits.pad(8, Nat.to_bits(len + offSet + 55))
|
||||
//log(Bits.show(Nat.to_bits(len + offSet + 55)) | " " | Bits.show(Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)))
|
||||
Bits.concat.go(len, binary_encoding)
|
||||
|
||||
@ -200,7 +31,7 @@ Ether.RPL.proof.encode.binary(value : Nat) : Bits
|
||||
if (value =? 0) then
|
||||
Bits.e
|
||||
else
|
||||
Bits.concat.go(Ether.RPL.proof.encode.binary(value / 256), Ether.RLP.pad_8bits(Nat.to_bits(value % 256)))
|
||||
Bits.concat.go(Ether.RPL.proof.encode.binary(value / 256), Ether.Bits.pad(8, Nat.to_bits(value % 256)))
|
||||
|
||||
Bits.break(len : Nat, bits : Bits) : Pair<Bits, Bits>
|
||||
{Bits.take(len, bits), Bits.drop(len, bits)}
|
||||
|
||||
@ -12,50 +12,85 @@ Bool.and.eq_sym(x : Bool, y : Bool, H : Equal(Bool, Bool.and(x, y), true)) : Pai
|
||||
Empty.absurd!(H)
|
||||
}!
|
||||
|
||||
Ether.RLP.Relation(x : Ether.RLP.Tree, y : Ether.RLP.Tree) : Type
|
||||
Ether.RLP.Tree.to_nat(x : Ether.RLP.Tree<Bits>) : Ether.RLP.Tree<Nat>
|
||||
case x {
|
||||
list : case y {
|
||||
list :
|
||||
Ether.RLP.Relation(
|
||||
?a
|
||||
tip : Empty
|
||||
}
|
||||
tip : case y {
|
||||
list : Empty
|
||||
tip : Bits.to_nat(x.value) == Bits.to_nat(y.value)
|
||||
}
|
||||
list : Ether.RLP.Tree.list!(List.map!!(Ether.RLP.Tree.to_nat, x.value))
|
||||
tip : Ether.RLP.Tree.tip!(Bits.to_nat(x.value))
|
||||
}
|
||||
|
||||
|
||||
Ether.RLP.section(tree : Ether.RLP.Tree) :
|
||||
Equal(Ether.RLP.Tree, Pair.fst!!(Ether.RLP.decode(Ether.RLP.encode(tree))), tree)
|
||||
case tree {
|
||||
tip :
|
||||
let e = refl ::
|
||||
Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.RLP.pad_bytes(tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.RLP.pad_bytes(tree.value))) == Ether.RLP.encode(Ether.RLP.Tree.tip(tree.value))
|
||||
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)
|
||||
let simpl = refl :: Nat.eql(Nat.mod(Bits.length(value),8),0,() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value)) == Ether.Bits.pad(8,value)
|
||||
case simpl {
|
||||
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)
|
||||
}!
|
||||
|
||||
Ether.RLP.section.tip_case(value : Bits, H : Bits.ltn(value,Ether.RLP.Constants.bits_128) == 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
|
||||
|
||||
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))
|
||||
case tree {
|
||||
tip :
|
||||
let e = refl :: Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))) == Ether.RLP.encode(Ether.RLP.Tree.tip(Bits,tree.value))
|
||||
case e {
|
||||
refl :
|
||||
let remember = case Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)) {
|
||||
true : (H)
|
||||
true : (H)
|
||||
let H = Bool.and.eq_sym!!(H)
|
||||
open H
|
||||
let H.snd = Equal.mirror(Bool, Bits.ltn(tree.value,Ether.RLP.Constants.bits_128), true, H.snd)
|
||||
case H.snd {
|
||||
refl :
|
||||
refl :
|
||||
let H.fst = Equal.mirror(Bool, Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), Bool.true, H.fst)
|
||||
case H.fst {
|
||||
refl : ?A-526-142
|
||||
} : Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(H.fst.b,Bool.true,() Bits,Ether.RLP.pad_bytes(tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.RLP.pad_bytes(tree.value))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
refl : _
|
||||
}!
|
||||
} : Ether.RLP.Tree.to_nat(Pair.fst(Ether.RLP.Tree(Bits),Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), H.snd.b,() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value)))))) == Ether.RLP.Tree.to_nat(Ether.RLP.Tree.tip(Bits,tree.value))
|
||||
false : _
|
||||
} : Equal(Bool, Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)), self) -> Ether.RLP.Tree.to_nat(Pair.fst(Ether.RLP.Tree(Bits),Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value)))))) == Ether.RLP.Tree.to_nat(Ether.RLP.Tree.tip(Bits,tree.value))
|
||||
remember(refl)
|
||||
}!
|
||||
list : _
|
||||
}!
|
||||
|
||||
// case tree {
|
||||
// tip :
|
||||
// let e = refl ::
|
||||
// Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))) == Ether.RLP.encode(Ether.RLP.Tree.tip(tree.value))
|
||||
// case e {
|
||||
// refl :
|
||||
// let remember = case Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)) {
|
||||
// true : (H)
|
||||
// let H = Bool.and.eq_sym!!(H)
|
||||
// open H
|
||||
// let H.snd = Equal.mirror(Bool, Bits.ltn(tree.value,Ether.RLP.Constants.bits_128), true, H.snd)
|
||||
// case H.snd {
|
||||
// refl :
|
||||
// let H.fst = Equal.mirror(Bool, Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), Bool.true, H.fst)
|
||||
// case H.fst {
|
||||
// refl : ?A-526-142
|
||||
// } : Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(H.fst.b,Bool.true,() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
|
||||
} : Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), H.snd.b,() Bits,Ether.RLP.pad_bytes(tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.RLP.pad_bytes(tree.value))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
false : (H) _
|
||||
} : Equal(Bool, Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)), self) -> Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.RLP.pad_bytes(tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.RLP.pad_bytes(tree.value))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
// } : Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1), H.snd.b,() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
// false : (H) _
|
||||
// } : Equal(Bool, Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128)), self) -> Pair.fst(Ether.RLP.Tree,Bits,Ether.RLP.decode(Bool.and(Nat.eql(Ether.Bits.get_bytes_size(tree.value),1),Bits.ltn(tree.value,Ether.RLP.Constants.bits_128),() Bits,Ether.Bits.pad(8,tree.value),Bits.concat.go(Ether.RPL.proof.encode_length(Ether.Bits.get_bytes_size(tree.value),128),Ether.Bits.pad(8,tree.value))))) == Ether.RLP.Tree.tip(tree.value)
|
||||
|
||||
|
||||
remember(refl)
|
||||
}!
|
||||
list : _
|
||||
}!
|
||||
// remember(refl)
|
||||
// }!
|
||||
// list : _
|
||||
// }!
|
||||
|
||||
|
||||
// case tree {
|
||||
|
||||
@ -1,18 +1,15 @@
|
||||
round_n(n : Nat, m : Nat) : Nat
|
||||
case Nat.lte(m, 8) {
|
||||
true : 8 - m
|
||||
false : round_n(n, m-8)
|
||||
}
|
||||
|
||||
Ether.tests : _
|
||||
let bits = Nat.to_bits(10002202234)
|
||||
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)))
|
||||
|
||||
let v = Ether.RLP.Tree.list(
|
||||
[
|
||||
Ether.RLP.Tree.tip(bits),
|
||||
Ether.RLP.Tree.tip(bits)
|
||||
])
|
||||
// let v = Ether.RLP.Tree.tip(Bits.read("1000000100000000000000000110110000000000000000000010000000000000000011011000111111111111111111111111111111111011111000000000000100011111111111111111111111111111111101111100000000000000000000000000000001000000000000000001101100100011111111111111111111111111111111101111100000000000010001111111111111111111111111111111110111110000000000000000000000000000000100000000000000000110110000000000000000000010000000000000000011011000000000000000000010110110"))
|
||||
let test1 = Ether.RLP.encode.bytes(v)
|
||||
//{test1, test2}
|
||||
|
||||
Ether.RLP.decode(test1)
|
||||
|
||||
//let buffer = Buffer8.from_hex("d69429d7d1dd5b6f9c864d9db560d72a247c178ae86b0a")
|
||||
//let hash = Crypto.Keccak.hash.bytes(buffer)
|
||||
//Buffer8.to_hex(hash)
|
||||
10
base/Logic/Equivalence.kind
Normal file
10
base/Logic/Equivalence.kind
Normal file
@ -0,0 +1,10 @@
|
||||
Logic.Equivalence.Relation (A : Type) : Type
|
||||
A -> A -> Type
|
||||
|
||||
type Logic.Equivalence(A : Type, R : Logic.Equivalence.Relation(A)) {
|
||||
new(
|
||||
reflexive : (x : A) -> R(x, x),
|
||||
symmetry : (x : A) -> (y : A) -> R(x, y) -> R(y, x)
|
||||
transivity : (x : A) -> (y : A) -> (z : A) -> R(x, y) -> R(y, z) -> R(x, z)
|
||||
)
|
||||
}
|
||||
13
base/Nat/eql/reflexivity.kind
Normal file
13
base/Nat/eql/reflexivity.kind
Normal file
@ -0,0 +1,13 @@
|
||||
Nat.eql.reflexivity(x : Nat, y : Nat, H : Nat.eql(x, y) == true) : x == y
|
||||
case x with H {
|
||||
succ : case y with H {
|
||||
succ : Equal.apply!!!!(Nat.succ, Nat.eql.reflexivity(x.pred, y.pred, H))
|
||||
zero :
|
||||
Empty.absurd!(Bool.false_neq_true(H))
|
||||
}!
|
||||
zero : case y with H {
|
||||
succ :
|
||||
Empty.absurd!(Bool.false_neq_true(H))
|
||||
zero : refl
|
||||
}!
|
||||
}!
|
||||
8
base/Nat/gte/gte_false.kind
Normal file
8
base/Nat/gte/gte_false.kind
Normal file
@ -0,0 +1,8 @@
|
||||
Nat.gte.gte_false(x : Nat, y : Nat, H : Nat.gte(x, y) == false) : Nat.gte(y, x) == true
|
||||
case x with H {
|
||||
succ : case y with H {
|
||||
succ : Nat.gte.gte_false(x.pred, y.pred, H)
|
||||
zero : Empty.absurd!(Bool.false_neq_true(mirror(H)))
|
||||
}!
|
||||
zero : refl
|
||||
}!
|
||||
13
base/Nat/lte/succ_both.kind
Normal file
13
base/Nat/lte/succ_both.kind
Normal file
@ -0,0 +1,13 @@
|
||||
Nat.lte.succ_both(x : Nat, y : Nat, H : Nat.lte(x, y) == true) : Nat.lte(Nat.succ(x), Nat.succ(y)) == true
|
||||
case y with H {
|
||||
zero :
|
||||
let H2 = Nat.lte.zero_right(x, H)
|
||||
let H2 = mirror(H2)
|
||||
case H2 {
|
||||
refl : refl
|
||||
} : Nat.lte(Nat.succ(H2.b),1) == Bool.true
|
||||
succ : case x with H {
|
||||
zero : refl
|
||||
succ : Nat.lte.succ_both(x.pred, y.pred, H)
|
||||
}!
|
||||
}!
|
||||
11
base/Nat/max/less.kind
Normal file
11
base/Nat/max/less.kind
Normal file
@ -0,0 +1,11 @@
|
||||
Nat.max.less(x : Nat, y : Nat) : (Nat.max(x, y) == x) -> Nat.lte(y, x) == true
|
||||
(H : Nat.lte(x,y,(self) Nat,y,x) == x) (case Nat.lte(x, y) {
|
||||
true : (Hyp)
|
||||
def H = H :: rewrite X in X((self) Nat, y, x) == x with Hyp
|
||||
let H = H :: y == x
|
||||
Nat.Order.refl(y) :: rewrite N in Nat.lte(y, N) == true with H
|
||||
false : (inverse)
|
||||
let inverse = Nat.lte.comm.false!!(inverse)
|
||||
let inverse = Nat.lte.succ_left!!(inverse)
|
||||
inverse
|
||||
} : (Nat.lte(x, y) == self) -> Nat.lte(y, x) == true)(refl)
|
||||
8
base/Nat/mod/le_mod.kind
Normal file
8
base/Nat/mod/le_mod.kind
Normal file
@ -0,0 +1,8 @@
|
||||
Nat.mod.le_mod(x : Nat, y : Nat, H : Nat.lte(Nat.succ(x), y) == true) : Nat.mod(x, y) == x
|
||||
let simpl = refl :: Pair.snd(Nat,Nat,Nat.lte(y,x,(self) Pair(Nat,Nat),Nat.div_mod.go(y,1,Nat.sub(x,y)),Pair.new(Nat,Nat,0,x))) == Nat.mod(x, y)
|
||||
let H2 = Nat.Order.trichotomy(y, x)
|
||||
case simpl {
|
||||
refl :
|
||||
let H = mirror(Nat.lte.comm.true!!(H))
|
||||
refl :: rewrite Y in Pair.snd(Nat,Nat,Y((self) Pair(Nat,Nat),Nat.div_mod.go(y,1,Nat.sub(x,y)),Pair.new(Nat,Nat,0,x))) == x with H
|
||||
}!
|
||||
@ -1,9 +1,9 @@
|
||||
//Nat.mod.small(
|
||||
// n: Nat
|
||||
// m: Nat
|
||||
// Hyp: Equal<Bool>(Nat.lte(1, m), true)
|
||||
//): Equal<Bool>(Nat.lte(m, Nat.mod(n, m)), false)
|
||||
// ?mod.small.body
|
||||
Nat.mod.small(
|
||||
n: Nat
|
||||
m: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(1, m), true)
|
||||
): Equal<Bool>(Nat.lte(m, Nat.mod(n, m)), false)
|
||||
Nat.mod.small.aux(m,0, n, Hyp)
|
||||
|
||||
Nat.mod.small.aux(
|
||||
n: Nat
|
||||
|
||||
Loading…
Reference in New Issue
Block a user