src/crypto/subtle.bend
1import 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.
17def 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.
25def 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))