Laws.spec_add_mod: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/laws.bend as Laws
Lines 21-26 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/laws.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/laws.bend&start_line=21&end_line=26

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

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

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/words.bend&name=add_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/words.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend&name=add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend&name=Lane