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 branch 'master' of github.com:uwu-tech/Kind

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-10 19:39:20 -03:00
commit fece62574d
3 changed files with 32 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
base/RLP.kind
View File

@ -63,6 +63,28 @@ RLP.decode.length(add: Nat, bytes: Bytes): Nat
new: got.snd
}
// Repeat
// ------
RLP.encode.repeat<A: Type>(encode: A -> Bytes, values: List<A>): Bytes
case values {
nil: []
cons: List.concat!(encode(values.head), RLP.encode.repeat<A>(encode, values.tail))
}
RLP.decoder.repeat<A: Type>(decoder: Bytes -> Pair<Bytes,A>, count: Nat, bytes: Bytes): Pair<Bytes, List<A>>
case count {
zero:
{bytes, []}
succ:
let {bytes, head} = decoder(bytes)
let {bytes, tail} = RLP.decoder.repeat<A>(decoder, count.pred, bytes)
{bytes, head & tail}
}
RLP.encode.many(trees: List<RLP>): Bytes
RLP.encode.repeat<RLP>(RLP.encode, trees)
// RLP
// ---
@ -98,25 +120,3 @@ RLP.decode(bytes: Bytes): RLP
case RLP.decoder(bytes) as got {
new: got.snd
}
// Repeat
// ------
RLP.encode.repeat<A: Type>(encode: A -> Bytes, values: List<A>): Bytes
case values {
nil: []
cons: List.concat!(encode(values.head), RLP.encode.repeat<A>(encode, values.tail))
}
RLP.decoder.repeat<A: Type>(decoder: Bytes -> Pair<Bytes,A>, count: Nat, bytes: Bytes): Pair<Bytes, List<A>>
case count {
zero:
{bytes, []}
succ:
let {bytes, head} = decoder(bytes)
let {bytes, tail} = RLP.decoder.repeat<A>(decoder, count.pred, bytes)
{bytes, head & tail}
}
RLP.encode.many(trees: List<RLP>): Bytes
RLP.encode.repeat<RLP>(RLP.encode, trees)

3
base/RLP/aux.kind
View File

@ -1,3 +1,6 @@
// These sub-theorems were not proven yet!
// Most of them are simple, and should be finished over the next days
// TODO: include `a <= 192`
RLP.aux.0(
add: Nat

14
base/RLP/encode_identity.kind
View File

@ -1,3 +1,10 @@
RLP.encode_identity(rlp: RLP): RLP.decode(RLP.encode(rlp)) == rlp
let pf = RLP.encode_identity.go(rlp, [])
let e0 = RLP.aux.16(RLP.encode(rlp))
let e1 = pf :: rewrite X in RLP.decoder(X) == Pair.new(Bytes,RLP,List.nil(U8),rlp) with e0
replace X with mirror(e1) in X((got) RLP,(got.fst) (got.snd) got.snd) == rlp
refl
RLP.encode_identity.go(rlp: RLP, bts: Bytes): Equal<Pair<Bytes,RLP>, RLP.decoder(List.concat<U8>(RLP.encode(rlp),bts)), Pair.new<Bytes,RLP>(bts,rlp)>
let ref_0 = RLP.encode_length_identity.go
let ref_1 = RLP.encode_repeat_identity.go
@ -63,10 +70,3 @@ RLP.encode_identity.go(rlp: RLP, bts: Bytes): Equal<Pair<Bytes,RLP>, RLP.decoder
refl
} : RLP.decoder(List.concat(U8,List.concat(U8,X,RLP.encode.many(rlp.child)),bts)) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
}!
RLP.encode_identity(rlp: RLP): RLP.decode(RLP.encode(rlp)) == rlp
let pf = RLP.encode_identity.go(rlp, [])
let e0 = RLP.aux.16(RLP.encode(rlp))
let e1 = pf :: rewrite X in RLP.decoder(X) == Pair.new(Bytes,RLP,List.nil(U8),rlp) with e0
replace X with mirror(e1) in X((got) RLP,(got.fst) (got.snd) got.snd) == rlp
refl