CORRECTNESS.bend source

CORRECTNESS.bend on the hub · documented module

import Baseimport ./buffer_proof.bend as BufferProofimport ./state.bend as Stateimport ./legacy_model.bend as SHAimport ./fips.bend as FIPSimport ./conformance.bend as Conformanceimport ./packed_proof.bend as PackedProofimport ./LAWS.bend as Laws# This gate contains NO concrete-message test vectors.def Laws.constants_correct():  {==}def Laws.sha256_correct(bytes):  Conformance.sha256_correct(bytes)law digest_octets_length:  for s: State.State  {List.length(&2, U32, FIPS.digest_octets(FIPS.digest(s))) == 32n : Nat}def digest_octets_length(s):  match s:    case State.H{a, b, c, d, e, f, g, h}:      {==}def Laws.digest_bytes_correct(ws):  match ws:    case Nil{}:      {==}    case w <> tail:      %Laws.digest_bytes_correct(tail) :        {SHA.digest_bytes(w <> tail) == List.append(&2, U32, FIPS.word_octets(w), _) : List<&2, U32>}      {==}def Laws.sha256_bytes_correct(bytes):  %Laws.sha256_correct(bytes) :    {SHA.sha256_bytes(bytes) == FIPS.digest_octets(_) : List<&2, U32>}  Laws.digest_bytes_correct(SHA.sha256(bytes))def Laws.sha256_bytes_length(bytes):  %Equal.sym(List<&2, U32>, SHA.sha256_bytes(bytes), FIPS.sha256_bytes(bytes), Laws.sha256_bytes_correct(bytes)) :    {List.length(&2, U32, _) == 32n : Nat}  digest_octets_length(FIPS.blocks(FIPS.prepare(bytes, 48n), FIPS.constants())(FIPS.initial()))def Laws.sha256_packed_correct(words,byte_length):  PackedProof.sha256_correct(words,byte_length)def Laws.sha256_array_correct(words,byte_length):  BufferProof.correct(words,byte_length)