proofs/crypto/sha512/words.bend

bend-collections-laws-crypto@1.0.0.0 · 42 lines · 3 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as FIPS
4import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
5import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
6import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-crypto@1.0.0.0/proofs/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
15def 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
20law carry_bit:
21  for +b: Bool
22  {X.b32(b) == Bool.to_u32(b) : U32}
23
24def carry_bit(b):
25  match b:
26    case True{}:
27      {==}
28    case False{}:
29      {==}
30
31law 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
36def 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})