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 theorem about list splitting

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-16 14:22:03 -03:00
parent f748820935
commit 0ce496c71f
4 changed files with 31 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
base/Bytes.kind
View File

@ -88,8 +88,3 @@ Bytes.inc(bytes: Bytes): Bytes
//e1: Nat.ltn(n, 256) == true
//): Equal<Bytes, Bytes.from_nat(n), [Nat.apply!(n, Word.inc<8>, Word.zero(8))]>
//Aux.1(n, e0, e1)

12
base/List/split/length.kind Normal file
View File

@ -0,0 +1,12 @@
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
cons:
let ind = List.split.length<A>(fst.tail, snd)
def split = List.split(A, fst.tail ++ snd, List.length<A>(fst.tail))
case split with ind: split == Pair.new!!(fst.tail, snd) {
new:
apply((p) open p Pair.new!!(fst.head & p.fst, p.snd), ind)
}! :: split!! == Pair.new!!(fst.head & fst.tail, snd)
}!

6
base/RLP.kind
View File

@ -43,8 +43,8 @@ RLP.show(r: RLP): String
// ------
RLP.encode.length(add: Nat, length: Nat): Bytes
if Nat.ltn(length, 56) then
Bytes.from_nat(Nat.add(add,length))
if Nat.lte(length, 55) then
[Nat.to_u8(Nat.add(add,length))]
else
let a = Bytes.from_nat(Nat.add(56, Nat.add(add, RLP.needed_bytes(length))))
let b = Bytes.from_nat(length)
@ -56,7 +56,7 @@ RLP.split.length(add: Nat, bytes: Bytes): Pair<Bytes, Bytes>
{[], []}
cons:
let fst = Nat.sub(U8.to_nat(bytes.head), add)
if Nat.ltn(fst, 56) then
if Nat.lte(fst, 55) then
Bytes.split(bytes.tail, fst)
else
let {length, tail} = Bytes.split(bytes.tail, Nat.sub(fst, 56))

24
base/RLP/aux.kind
View File

@ -4,15 +4,23 @@ 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!(payload)) ++ payload ++ tail) == {payload, tail}
?test
): 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.1(
payload: Bytes
tail: Bytes
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
): RLP.split.length(128, RLP.encode.length(128, List.length!(payload)) ++ payload ++ tail) == {payload, tail}
?test
//RLP.aux.split.1(
// payload: Bytes
// tail: Bytes
// H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
//): RLP.split.length(128, RLP.encode.length(128, List.length!(payload)) ++ payload ++ tail) == {payload, tail}
// ?test
// TODO: include `a <= 192`
//RLP.aux.0(