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

make definitions more amenable to verification

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-16 20:42:54 -03:00
parent 12c95ee21d
commit 1036ca7c30
2 changed files with 7 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
base/Bytes.kind
View File

@ -30,14 +30,13 @@ Bytes.to_nat(bytes: Bytes): Nat
Nat.add(head, Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(tail)))))))))
}
Bytes.from_nat.go(n: Nat, r: Bytes): Bytes
case n {
zero: r
succ: Bytes.from_nat.go(n.pred, Bytes.inc(r))
}
Bytes.from_nat(n: Nat): Bytes
Bytes.from_nat.go(n, [])
case n {
zero:
List.nil!
succ:
Bytes.from_nat(n/256) ++ [U8.from_nat(Nat.mod(n, 256))]
}
Bytes.to_hex(b: Bytes): String
Bytes.to_hex.go("", b)

2
base/RLP/aux.kind
View File

@ -15,7 +15,7 @@ RLP.aux.split.0(
refl:
List.split.length(U8, payload, tail)
}: H.b(() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,List.nil(U8),List.concat(U8,payload,tail)), List.length(U8, payload)),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)
}: Nat.lte(recover_num.b,55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,List.nil(U8),List.concat(U8,payload,tail)), recover_num.b),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)
}: Nat.lte( recover_num.b ,55,() Pair(Bytes,Bytes),Bytes.split(List.concat(U8,List.nil(U8),List.concat(U8,payload,tail)), recover_num.b ),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,List.concat(U8, H.b( () 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(