1	import Base
2	import ../../../src/crypto/sha512/types.bend as T
3	import ../../../spec/crypto/sha512.bend as FIPS
4	import ../../../spec/lib/common.bend as C
5	import ../../../src/math/w64.bend as X
6	import ../../../src/math/u64.bend as WU
7	import ../../math/typed/w64add.bend as W64A
8	
9	# The specification's 64-bit words mean what FIPS 180-4 section 3.2 says: a
10	# word W{hi, lo} is the number lo + 2^32 hi, and the specification's addition
11	# is addition modulo 2^64. This does not rest on the implementation: it is
12	# the proved U64 addition of src/math/w64.bend (spec/math/w64.bend Add.value,
13	# proofs/math/typed/w64add.bend), which computes the same halves.
14	
15	def value(w: T.Lane) -> Nat:
16	  match w:
17	    case T.W{hi, lo}:
18	      Nat.add(U32.to_nat(lo), C.shift(32n, U32.to_nat(hi)))
19	
20	law carry_bit:
21	  for +b: Bool
22	  {X.b32(b) == Bool.to_u32(b) : U32}
23	
24	def carry_bit(b):
25	  match b:
26	    case True{}:
27	      {==}
28	    case False{}:
29	      {==}
30	
31	law add_value:
32	  for +a: T.Lane
33	  for +b: T.Lane
34	  {value(FIPS.add(a, b)) == C.low(64n, Nat.add(value(a), value(b))) : Nat}
35	
36	def add_value(a, b):
37	  match a b:
38	    case T.W{ah, al} T.W{bh, bl}:
39	      %carry_bit(U32.is_lt(U32.add(al, bl), al)) :
40	        {Nat.add(U32.to_nat(U32.add(al, bl)), C.shift(32n, U32.to_nat(U32.add(U32.add(ah, bh), _)))) ==
41	          C.low(64n, Nat.add(value(T.W{ah, al}), value(T.W{bh, bl}))) : Nat}
42	      W64A.add_value(WU.U64{al, ah}, WU.U64{bl, bh})