proofs/crypto/sha512/words.bend source

proofs/crypto/sha512/words.bend on the hub · documented module

import Baseimport ../../../src/crypto/sha512/types.bend as Timport ../../../spec/crypto/sha512.bend as FIPSimport ../../../spec/lib/common.bend as Cimport ../../../src/math/w64.bend as Ximport ../../../src/math/u64.bend as WUimport ../../math/typed/w64add.bend as W64A# The specification's 64-bit words mean what FIPS 180-4 section 3.2 says: a# word W{hi, lo} is the number lo + 2^32 hi, and the specification's addition# is addition modulo 2^64. This does not rest on the implementation: it is# the proved U64 addition of src/math/w64.bend (spec/math/w64.bend Add.value,# proofs/math/typed/w64add.bend), which computes the same halves.def value(w: T.Lane) -> Nat:  match w:    case T.W{hi, lo}:      Nat.add(U32.to_nat(lo), C.shift(32n, U32.to_nat(hi)))law carry_bit:  for +b: Bool  {X.b32(b) == Bool.to_u32(b) : U32}def carry_bit(b):  match b:    case True{}:      {==}    case False{}:      {==}law add_value:  for +a: T.Lane  for +b: T.Lane  {value(FIPS.add(a, b)) == C.low(64n, Nat.add(value(a), value(b))) : Nat}def add_value(a, b):  match a b:    case T.W{ah, al} T.W{bh, bl}:      %carry_bit(U32.is_lt(U32.add(al, bl), al)) :        {Nat.add(U32.to_nat(U32.add(al, bl)), C.shift(32n, U32.to_nat(U32.add(U32.add(ah, bh), _)))) ==          C.low(64n, Nat.add(value(T.W{ah, al}), value(T.W{bh, bl}))) : Nat}      W64A.add_value(WU.U64{al, ah}, WU.U64{bl, bh})