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

bound length of subencodings

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-22 12:40:08 -03:00
parent 1ff9f8210b
commit da36a89740
6 changed files with 111 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
base/List/concat.kind
View File

@ -3,7 +3,6 @@
// as = [3, 4]
// bs = [1, 2]
// List.concat<Nat>(as, bs) == [3, 4, 1, 2]
List.concat<A: Type>(as: List<A>, bs: List<A>): List<A>
case as {
nil: bs,

13
base/List/concat/length.kind Normal file
View File

@ -0,0 +1,13 @@
List.concat.length<A: Type>(
l0: List<A>, l1: List<A>
): Equal<Nat>(Nat.add(List.length<A>(l0), List.length<A>(l1)), List.length<A>(List.concat<A>(l0, l1)))
case l0 {
nil:
refl
cons:
let ind = List.concat.length<A>(l0.tail, l1)
case ind {
refl:
refl
}: Equal<Nat>(Nat.succ(Nat.add(List.length<A>(l0.tail), List.length<A>(l1))), Nat.succ(ind.b))
}!

13
base/Nat/lte/cut_left.kind Normal file
View File

@ -0,0 +1,13 @@
Nat.lte.cut_left(
a: Nat
b: Nat
c: Nat
H: Equal(Bool, Nat.lte(Nat.add(a, b), c), true)
): Equal(Bool, Nat.lte(b, c), true)
case a with H {
zero:
H
succ:
let lemma = Nat.lte.succ_left(Nat.add(a.pred, b), c, H)
Nat.lte.cut_left(a.pred, b, c, lemma)
}!

10
base/Nat/lte/cut_right.kind Normal file
View File

@ -0,0 +1,10 @@
Nat.lte.cut_right(
a: Nat
b: Nat
c: Nat
H: Equal(Bool, Nat.lte(Nat.add(a, b), c), true)
): Equal(Bool, Nat.lte(a, c), true)
case Nat.add.comm(b, a) with H: Nat.lte(self.b, c) == true {
refl:
Nat.lte.cut_left(b, a, c, H)
}!

72
base/RLP/bound_encoding.kind Normal file
View File

@ -0,0 +1,72 @@
RLP.bound_encoding(
rlps: List<RLP>, bound: Nat
H: Equal(Bool, Nat.lte(List.length(U8, RLP.encode.many(rlps)), bound), true)
): RLP.bound_encoding.type(rlps, bound)
Pair.new!!(
H
case rlps with H {
nil:
unit
cons:
Pair.new!!(
case rlps.head with H {
data:
let split_concat = List.concat.length<U8>(RLP.encode(RLP.data(rlps.head.value)), RLP.encode.many(rlps.tail))
case split_concat with H: Nat.lte(split_concat.b, bound) == true {
refl:
let H = Nat.lte.cut_right(List.length(U8,RLP.encode(RLP.data(rlps.head.value))),List.length(U8,RLP.encode.many(rlps.tail)),bound, H)
def condition = Bool.and(Nat.eql(List.length!(rlps.head.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 127))
case condition with H: Nat.lte(List.length(U8, condition(() Bytes, rlps.head.value, List.concat(U8, RLP.encode.length(128, List.length(U8, rlps.head.value)), rlps.head.value))), bound) == true {
true:
H
false:
let split_concat = List.concat.length<U8>(RLP.encode.length(128,List.length(U8,rlps.head.value)), rlps.head.value)
case split_concat with H: Nat.lte(split_concat.b,bound) == Bool.true {
refl:
let H = Nat.lte.cut_left(List.length(U8,RLP.encode.length(128,List.length(U8,rlps.head.value))),List.length(U8,rlps.head.value),bound, H)
H
}!
}!
}! :: Nat.lte(List.length(U8,rlps.head.value),bound) == true
node:
let split_concat = List.concat.length<U8>(RLP.encode(RLP.node(rlps.head.child)), RLP.encode.many(rlps.tail))
case split_concat with H: Nat.lte(split_concat.b, bound) == true {
refl:
let H = Nat.lte.cut_right(List.length(U8,RLP.encode(RLP.node(rlps.head.child))),List.length(U8,RLP.encode.many(rlps.tail)), bound, H)
let split_concat =
List.concat.length<U8>(RLP.encode.length(192, List.length(U8, RLP.encode.many(rlps.head.child))), RLP.encode.many(rlps.head.child))
case split_concat with H: Nat.lte(split_concat.b, bound) == true {
refl:
let H = Nat.lte.cut_left(List.length(U8,RLP.encode.length(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.length(U8,RLP.encode.many(rlps.head.child)), bound, H)
RLP.bound_encoding(rlps.head.child, bound, H)
}!
}! :: RLP.bound_encoding.type(rlps.head.child,bound)
}! :: rlps.head!!!
let H = H :: Nat.lte(List.length(U8,List.concat(U8, RLP.encode(rlps.head), RLP.encode.many(rlps.tail))),bound) == true
case List.concat.length<U8>(RLP.encode(rlps.head), RLP.encode.many(rlps.tail)) with H: Nat.lte(self.b, bound) == true {
refl:
let H = Nat.lte.cut_left(List.length(U8, RLP.encode(rlps.head)), List.length(U8, RLP.encode.many(rlps.tail)), bound, H)
RLP.bound_encoding(rlps.tail, bound, H)
}!
)
}! :: rlps!!!
)
RLP.bound_encoding.type(rlps: List<RLP>, bound: Nat): Type
And<
Equal<Bool>(Nat.lte(List.length(U8, RLP.encode.many(rlps)), bound), true)
case rlps {
nil:
Unit
cons:
And<
case rlps.head {
data:
Equal(Bool, Nat.lte(List.length(U8, rlps.head.value), bound), true)
node:
RLP.bound_encoding.type(rlps.head.child, bound)
}
RLP.bound_encoding.type(rlps.tail, bound)
>
}
>

5
base/Word/to_nat/safe.kind
View File

@ -1,4 +1,5 @@
// TODO
Word.to_nat.safe<size: Nat>(
n: Nat, H: Nat.lte(Nat.succ(n), Nat.pow(2, size)) == true
): Word.to_nat(Nat.to_word(size, n)) == n
?word.to_nat.safe
): n == Word.to_nat(size, Nat.to_word(size, n))
Word.to_nat.safe(size, n, H)