spec/crypto/subtle.bend

bend-collections-laws-crypto@1.0.0.0 · 20 lines · 1 definition

1import Base
2
3# Specification of src/crypto/subtle.bend: list equality, decided position by
4# position (the reference; it may stop at the first difference, the
5# implementation may not). Clauses in proofs/crypto/subtle/laws.bend:
6#
7#   Eq.value  eq(a, b) == equal(a, b)            (the Bool it returns)
8#   Eq.sound  eq(a, b) == True  implies  a == b  (as lists)
9#   Eq.refl   eq(a, a) == True
10#
11# Together: eq(a, b) is True exactly when a == b.
12
13def equal(a: List<&2, U32>, b: List<&2, U32>) -> Bool:
14  match a b:
15    case Nil{} Nil{}:
16      True{}
17    case x <> xs y <> ys:
18      Bool.and(U32.is_eq(x, y), equal(xs, ys))
19    case _ _:
20      False{}