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

merge my work with tiago's

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-16 15:56:26 -03:00
parent b94f4770c6
commit 574d42b2ae
5 changed files with 23 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
base/List/split/length.kind
View File

@ -1,4 +1,6 @@
List.split.length<A: Type>(fst: List<A>, snd: List<A>): List.split<A>(fst ++ snd, List.length<A>(fst)) == Pair.new!!(fst, snd)
List.split.length<A: Type>(
fst: List<A>, snd: List<A>
): List.split<A>(fst ++ snd, List.length<A>(fst)) == Pair.new!!(fst, snd)
case fst {
nil:
refl

8
base/Nat/ltn.kind
View File

@ -1,8 +1,2 @@
Nat.ltn(n: Nat, m: Nat): Bool
case m {
zero: Bool.false,
succ: case n {
zero: Bool.true,
succ: Nat.ltn(n.pred, m.pred),
}
}
Nat.lte(Nat.succ(n), m)

31
base/RLP/aux.kind
View File

@ -1,20 +1,21 @@
// These sub-theorems were not proven yet!
// Most of them are simple, and should be finished over the next days
// RLP.aux.split.0(
// payload: Bytes
// tail: Bytes
// H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
// ): RLP.split.length(128, RLP.encode.length(128, List.length<U8>(payload)) ++ payload ++ tail) == {payload, tail}
// case Nat.lte(List.length<U8>(payload), 55) with H {
// true:
// //?test ::
// // RLP.split.length(128, Bytes.from_nat(Nat.add(128, length)) ++ payload ++ tail) == {payload, tail}
// // Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128, length))), 128)!!! == {payload, tail}
// // Bytes.split(payload ++ tail, List.length!(payload))
// _
// false:
// Empty.absurd!(Bool.false_neq_true(H))
// }! :: RLP.split.length(128, Nat.lte(List.length<U8>(payload), 55)!!! ++ payload ++ tail) == {payload, tail}
RLP.aux.split.0(
payload: Bytes
tail: Bytes
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
): RLP.split.length(128, RLP.encode.length(128, List.length<U8>(payload)) ++ payload ++ tail) == {payload, tail}
case Nat.lte(List.length<U8>(payload), 55) with H {
true:
def fst = Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,payload)))),128)
?test :: Nat.lte(fst,55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,List.nil(U8),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,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, Bytes.from_nat(Nat.add(128, length)) ++ payload ++ tail) == {payload, tail}
// Nat.sub(U8.to_nat(Nat.to_u8(Nat.add(128, length))), 128)!!! == {payload, tail}
// Bytes.split(payload ++ tail, List.length!(payload))
false:
Empty.absurd!(Bool.false_neq_true(H))
}! :: RLP.split.length(128,List.concat(U8,Nat.lte(List.length(U8,payload),55,() 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)
RLP.aux.split.1(
payload: Bytes

3
base/RLP/encode_identity.kind
View File

@ -44,7 +44,8 @@ RLP.encode_identity(rlp: RLP): RLP.decode(RLP.encode(rlp)) == rlp
} : RLP.decode(List.concat(U8,X,rlp.value)) == RLP.data(rlp.value)
} : RLP.decode(X(() List(U8),rlp.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlp.value)),rlp.value))) == RLP.data(rlp.value)
node : _
node :
?node
}!

10
base/Test.kind
View File

@ -1,10 +1,2 @@
Test: _
let a = RLP.encode
let b = RLP.decode
0
//let a = RLP.encode(RLP.data([0x80#8,0x80#8,0x80#8]))
//let b = RLP.decode(a)
//{
//Bytes.show(a)
//b
//}
[0] ++ [1]