1	import 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	
13	def 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{}