mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-11-05 07:05:32 +03:00
Merge branch 'master' of github.com:kind-lang/kind
This commit is contained in:
MaiaVictor
commit
85cbac15c1
31
base/Bits/cmp/identity_by_o.kind
Normal file
31
base/Bits/cmp/identity_by_o.kind
Normal file
@ -0,0 +1,31 @@
|
||||
Bits.cmp.identity_by_o.aux.left(y : Bits) : Bits.cmp.go(Bits.e,y,Cmp.ltn) == Cmp.ltn
|
||||
case y {
|
||||
e : refl
|
||||
o : Bits.cmp.identity_by_o.aux.left(y.pred)
|
||||
i : refl
|
||||
}!
|
||||
|
||||
Bits.cmp.identity(x : Bits, y : Bits, j : Cmp, j2 : Cmp, H : Bits.cmp.go(x, y, j) == j2)
|
||||
: Bits.cmp.go(Bits.trim.insert(x), y, j) == j2
|
||||
case x with H {
|
||||
o :
|
||||
case y with H {
|
||||
i : Bits.cmp.identity(x.pred, y.pred, Cmp.ltn, j2, H)
|
||||
o : Bits.cmp.identity(x.pred, y.pred, j, j2, H)
|
||||
e : Bits.cmp.identity(x.pred, Bits.e, j, j2, H)
|
||||
}!
|
||||
i : case y with H {
|
||||
i : Bits.cmp.identity(x.pred, y.pred, j, j2, H)
|
||||
o : Bits.cmp.identity(x.pred, y.pred, Cmp.gtn, j2, H)
|
||||
e : H
|
||||
}!
|
||||
e : case y with H {
|
||||
i :
|
||||
let H = H :: Cmp.ltn == j2
|
||||
case H {
|
||||
refl : Bits.cmp.identity_by_o.aux.left(y.pred)
|
||||
}!
|
||||
o : H
|
||||
e : H
|
||||
}!
|
||||
}!
|
||||
@ -1,62 +1,65 @@
|
||||
// This function is fully expanded for max performance
|
||||
Bits.hex.encode(x: Bits): String
|
||||
Bits.hex.encode.go("", x)
|
||||
|
||||
Bits.hex.encode.go(acc: String, x: Bits): String
|
||||
case x {
|
||||
e: ""
|
||||
e: acc
|
||||
o: case x.pred as x {
|
||||
e: "0"
|
||||
e: acc|"0"
|
||||
o: case x.pred as x {
|
||||
e: "0"
|
||||
e: acc|"0"
|
||||
o: case x.pred as x {
|
||||
e: "0"
|
||||
o: "0" | Bits.hex.encode(x.pred)
|
||||
i: "8" | Bits.hex.encode(x.pred)
|
||||
e: acc|"0"
|
||||
o: Bits.hex.encode.go(acc|"0", x.pred)
|
||||
i: Bits.hex.encode.go(acc|"8", x.pred)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "4"
|
||||
o: "4" | Bits.hex.encode(x.pred)
|
||||
i: "c" | Bits.hex.encode(x.pred)
|
||||
e: acc|"4"
|
||||
o: Bits.hex.encode.go(acc|"4", x.pred)
|
||||
i: Bits.hex.encode.go(acc|"c", x.pred)
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "2"
|
||||
e: acc|"2"
|
||||
o: case x.pred as x {
|
||||
e: "2"
|
||||
o: "2" | Bits.hex.encode(x.pred)
|
||||
i: "a" | Bits.hex.encode(x.pred)
|
||||
e: acc|"2"
|
||||
o: Bits.hex.encode.go(acc|"2", x.pred)
|
||||
i: Bits.hex.encode.go(acc|"a", x.pred)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "6"
|
||||
o: "6" | Bits.hex.encode(x.pred)
|
||||
i: "e" | Bits.hex.encode(x.pred)
|
||||
e: acc|"6"
|
||||
o: Bits.hex.encode.go(acc|"6", x.pred)
|
||||
i: Bits.hex.encode.go(acc|"e", x.pred)
|
||||
}
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "1"
|
||||
e: acc|"1"
|
||||
o: case x.pred as x {
|
||||
e: "1"
|
||||
e: acc|"1"
|
||||
o: case x.pred as x {
|
||||
e: "1"
|
||||
o: "1" | Bits.hex.encode(x.pred)
|
||||
i: "9" | Bits.hex.encode(x.pred)
|
||||
e: acc|"1"
|
||||
o: Bits.hex.encode.go(acc|"1", x.pred)
|
||||
i: Bits.hex.encode.go(acc|"9", x.pred)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "5"
|
||||
o: "5" | Bits.hex.encode(x.pred)
|
||||
i: "d" | Bits.hex.encode(x.pred)
|
||||
e: acc|"5"
|
||||
o: Bits.hex.encode.go(acc|"5", x.pred)
|
||||
i: Bits.hex.encode.go(acc|"d", x.pred)
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "3"
|
||||
e: acc|"3"
|
||||
o: case x.pred as x {
|
||||
e: "3"
|
||||
o: "3" | Bits.hex.encode(x.pred)
|
||||
i: "b" | Bits.hex.encode(x.pred)
|
||||
e: acc|"3"
|
||||
o: Bits.hex.encode.go(acc|"3", x.pred)
|
||||
i: Bits.hex.encode.go(acc|"b", x.pred)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "7"
|
||||
o: "7" | Bits.hex.encode(x.pred)
|
||||
i: "f" | Bits.hex.encode(x.pred)
|
||||
e: acc|"7"
|
||||
o: Bits.hex.encode.go(acc|"7", x.pred)
|
||||
i: Bits.hex.encode.go(acc|"f", x.pred)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -6,4 +6,11 @@ Bits.trim(new_len: Nat, bits: Bits): Bits
|
||||
o: Bits.o(Bits.trim(new_len.pred, bits.pred)),
|
||||
i: Bits.i(Bits.trim(new_len.pred, bits.pred)),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Bits.trim.insert(bits: Bits): Bits
|
||||
case bits {
|
||||
e : Bits.o(Bits.e)
|
||||
o : Bits.o(Bits.trim.insert(bits.pred))
|
||||
i : Bits.i(Bits.trim.insert(bits.pred))
|
||||
}
|
||||
|
||||
23
base/Bits/trim/identity.kind
Normal file
23
base/Bits/trim/identity.kind
Normal file
@ -0,0 +1,23 @@
|
||||
Bits.trim.identity(bits : Bits) : Bits.trim(Bits.length(bits), bits) == bits
|
||||
case bits {
|
||||
e : refl
|
||||
o :
|
||||
let rec = Bits.trim.identity(bits.pred)
|
||||
case refl :: Bits.length.go(bits.pred,1) == Bits.length(Bits.o(bits.pred)) {
|
||||
refl :
|
||||
let H = Bits.length.succ(bits.pred, 0)
|
||||
case H {
|
||||
refl : Equal.apply!!!!(Bits.o, rec)
|
||||
}!
|
||||
}!
|
||||
|
||||
i :
|
||||
let rec = Bits.trim.identity(bits.pred)
|
||||
case refl :: Bits.length.go(bits.pred,1) == Bits.length(Bits.i(bits.pred)) {
|
||||
refl :
|
||||
let H = Bits.length.succ(bits.pred, 0)
|
||||
case H {
|
||||
refl : Equal.apply!!!!(Bits.i, rec)
|
||||
}!
|
||||
}!
|
||||
}!
|
||||
22
base/Cmp/equal.kind
Normal file
22
base/Cmp/equal.kind
Normal file
@ -0,0 +1,22 @@
|
||||
Cmp.equal(x : Cmp, y : Cmp) : Bool
|
||||
case x {
|
||||
gtn : Cmp.as_gtn(y)
|
||||
ltn : Cmp.as_ltn(y)
|
||||
eql : Cmp.as_eql(y)
|
||||
}
|
||||
|
||||
Cmp.equal.absurd(x : Cmp, y : Cmp, H : x == y, H2 : Cmp.equal(x, y) == false) : Empty
|
||||
case x with H H2 {
|
||||
gtn :
|
||||
case H with H2 {
|
||||
refl : Empty.absurd!(Bool.false_neq_true(mirror(H2)))
|
||||
}!
|
||||
ltn :
|
||||
case H with H2 {
|
||||
refl : Empty.absurd!(Bool.false_neq_true(mirror(H2)))
|
||||
}!
|
||||
eql :
|
||||
case H with H2 {
|
||||
refl : Empty.absurd!(Bool.false_neq_true(mirror(H2)))
|
||||
}!
|
||||
}!
|
||||
@ -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
|
||||
|
||||
@ -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))
|
||||
|
||||
@ -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")
|
||||
|
||||
@ -29,7 +29,7 @@ User.rigille.List.Monotone.exists<A: Type>(after: A -> A -> Type, O: User.rigill
|
||||
def ret = ext.fst & tail_call.fst
|
||||
|
||||
// prove return value is a permutation
|
||||
let ret_perm = (lem_left = User.rigille.List.Perm.refl<A>(xs.head & xs.tail)
|
||||
let ret_perm = (let lem_left = User.rigille.List.Perm.refl<A>(xs.head & xs.tail)
|
||||
// Perm(min_split.fst ++ [ext.fst] ++ min_split.snd.fst, xs.head & xs.tail)
|
||||
let lem_right = lem_left :: rewrite X in Perm(X, _) with min_split.snd.snd
|
||||
// Perm([ext.fst] ++ min_split.fst, min_split.fst ++ [ext.fst])
|
||||
@ -54,10 +54,10 @@ User.rigille.List.Monotone.exists<A: Type>(after: A -> A -> Type, O: User.rigill
|
||||
let ret_monotone = case tail_call.fst
|
||||
with tail_call.snd.snd
|
||||
ret_perm {
|
||||
nil: qed = unit :: User.rigille.List.Monotone<A, after, O>(ext.fst & [])
|
||||
nil: let qed = unit :: User.rigille.List.Monotone<A, after, O>(ext.fst & [])
|
||||
qed
|
||||
|
||||
cons: in_tail_call = right(left(refl)) :: User.rigille.List.In<A>(ext.fst & tail_call.fst.head & tail_call.fst.tail, tail_call.fst.head)
|
||||
cons: let in_tail_call = right(left(refl)) :: User.rigille.List.In<A>(ext.fst & tail_call.fst.head & tail_call.fst.tail, tail_call.fst.head)
|
||||
let in_param = User.rigille.List.Perm.In<A>(_, _, _,
|
||||
in_tail_call, User.rigille.List.Perm.symm<A>(_, _, ret_perm))
|
||||
let qed = ext.snd.snd(_, in_param)
|
||||
|
||||
@ -4,11 +4,11 @@ User.rigille.List.Perm.cat_comm<A: Type>(
|
||||
): User.rigille.List.Perm<A>(ys ++ xs, xs ++ ys)
|
||||
def Perm = User.rigille.List.Perm<A>
|
||||
case xs {
|
||||
nil: lem = User.rigille.List.Perm.refl<A>(ys)
|
||||
nil: let lem = User.rigille.List.Perm.refl<A>(ys)
|
||||
let calc = User.rigille.List.cat_l_nil!(ys)
|
||||
let qed = lem :: rewrite X in (Perm(X, ys)) with calc
|
||||
qed
|
||||
cons: ind = User.rigille.List.Perm.cat_comm<A>(xs.tail, ys)
|
||||
cons: let ind = User.rigille.List.Perm.cat_comm<A>(xs.tail, ys)
|
||||
let lem_right = User.rigille.List.Perm.skip<A>(xs.head, _, _, ind)
|
||||
let lem_left = User.rigille.List.Perm.front_to_back<A>(xs.head, ys)
|
||||
let lem_left = User.rigille.List.Perm.push_tail<A>(_, _, xs.tail, lem_left)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user