spec/crypto/subtle.bend source

spec/crypto/subtle.bend on the hub · documented module

import Base# Specification of src/crypto/subtle.bend: list equality, decided position by# position (the reference; it may stop at the first difference, the# implementation may not). Clauses in proofs/crypto/subtle/laws.bend:##   Eq.value  eq(a, b) == equal(a, b)            (the Bool it returns)#   Eq.sound  eq(a, b) == True  implies  a == b  (as lists)#   Eq.refl   eq(a, a) == True## Together: eq(a, b) is True exactly when a == b.def equal(a: List<&2, U32>, b: List<&2, U32>) -> Bool:  match a b:    case Nil{} Nil{}:      True{}    case x <> xs y <> ys:      Bool.and(U32.is_eq(x, y), equal(xs, ys))    case _ _:      False{}