1	import Base
2	import ../../../src/crypto/subtle.bend as Subtle
3	import ../../../spec/crypto/subtle.bend as Spec
4	
5	# The clauses of spec/crypto/subtle.bend. Proved in proof.bend.
6	
7	# eq returns the reference list equality.
8	law Eq.value:
9	  for +a: List<&2, U32>
10	  for +b: List<&2, U32>
11	  {Subtle.eq(a, b) == Spec.equal(a, b) : Bool}
12	
13	# eq is True only for equal lists.
14	law Eq.sound:
15	  for +a: List<&2, U32>
16	  for +b: List<&2, U32>
17	  for +h: {Subtle.eq(a, b) == True{} : Bool}
18	  {a == b : List<&2, U32>}
19	
20	# eq is True on equal lists.
21	law Eq.refl:
22	  for +a: List<&2, U32>
23	  {Subtle.eq(a, a) == True{} : Bool}