proofs/crypto/subtle/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 23 lines · 3 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as Spec
4
5# The clauses of spec/crypto/subtle.bend. Proved in proof.bend.
6
7# eq returns the reference list equality.
8law Eq.value:
9  for +a: List<&2, U32>
10  for +b: List<&2, U32>
11  {Subtle.eq(a, b) == Spec.equal(a, b) : Bool}
12
13# eq is True only for equal lists.
14law Eq.sound:
15  for +a: List<&2, U32>
16  for +b: List<&2, U32>
17  for +h: {Subtle.eq(a, b) == True{} : Bool}
18  {a == b : List<&2, U32>}
19
20# eq is True on equal lists.
21law Eq.refl:
22  for +a: List<&2, U32>
23  {Subtle.eq(a, a) == True{} : Bool}