1	import Base
2	
3	# Constant-time comparison of byte strings, after Go's crypto/subtle
4	# (ConstantTimeCompare) and HACL*'s Lib.ByteBuffer.lbytes_eq.
5	#
6	# Bytes are U32 values (each < 256 in the byte convention; any U32 works).
7	# The lengths are public: lists of different lengths are unequal, decided on
8	# the lengths alone. For equal lengths, every position is read: the XOR of
9	# the two bytes is ORed into an accumulator, with no early exit and no branch
10	# on the contents, and the result is whether the accumulator is zero.
11	#
12	# Bend has no timing model, so "constant time" is a property of this code's
13	# shape (one pass, no data-dependent match), not a proved fact. What is proved
14	# (proofs/crypto/subtle/) is its value: eq(a, b) is True exactly when a == b.
15	
16	# OR of the XOR of every pair of positions, over the common prefix.
17	def diff(a: List<&2, U32>, b: List<&2, U32>, acc: U32) -> U32:
18	  match a b:
19	    case x <> xs y <> ys:
20	      diff(xs, ys, U32.or(acc, U32.xor(x, y)))
21	    case _ _:
22	      acc
23	
24	# True exactly when a and b are the same list.
25	def eq(+a: List<&2, U32>, +b: List<&2, U32>) -> Bool:
26	  Bool.and(Nat.is_eq(List.length(&2, U32, a), List.length(&2, U32, b)),
27	    U32.is_eq(diff(a, b, 0), 0))