law spec_add_mod

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha512/laws.bend:21

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as FIPS
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/words.bend as Words

21# The specification's word addition is addition modulo 2^64 (FIPS 180-4
22# section 3.2), with W{hi, lo} read as lo + 2^32 hi.
23law spec_add_mod:
24  for +a: T.Lane
25  for +b: T.Lane
26  {Words.value(FIPS.add(a, b)) == C.low(64n, Nat.add(Words.value(a), Words.value(b))) : Nat}