~/bend-docscommunity

proofs/crypto/sha/packed/buffer_proof.bend fails

raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/buffer_proof.bend as Buffer_proof

9 imports
import Base
import ../../../../spec/crypto/sha.bend as F
import ../../../../src/crypto/sha/packed/buffer.bend as B
import ../../../../src/crypto/sha/packed/packed.bend as P
import ../../../../spec/crypto/sha/packed.bend as R
import ./packed_proof.bend as Proof
import ./packed_array_proof.bend as A
import ../../../../src/crypto/sha/state.bend as S
import ../../../../src/crypto/sha/packed/sha256.bend as SHA

Laws

law correct unverifiedits file does not pass the checker (fails)source · line 11 · raw

@a:Array<U32> -> @+length:Nat -> {0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/sha256.sha256(a, length) == 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/buffer.result(0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha/packed.hash(a, length)) : Maybe<&1, Array<U32>>}

law digest_size unverifiedits file does not pass the checker (fails)source · line 20 · raw

@s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> {Pair.snd(Array<U32>, U32, Array.size(U32, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/buffer.digest(s))) == 8 : U32}

law digest_words unverifiedits file does not pass the checker (fails)source · line 34 · raw

@+s:0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State -> {words(0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/buffer.digest(s)) == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha.digest(s) : List<&2, U32>}

law observe_digest unverifiedits file does not pass the checker (fails)source · line 48 · raw

@+r:Maybe<&2, 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.State> -> {observe(0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/buffer.result(r)) == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha/packed.digest_result(r) : Maybe<&2, List<&2, U32>>}

law full_reified unverifiedits file does not pass the checker (fails)source · line 59 · raw

@-a:Array<U32> -> @+length:Nat -> @view:Sigma<&2, &1, 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/packed_array_proof.Tree, t => {a == 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/packed_array_proof.thaw(t) : Array<U32>}> -> {observe(0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/sha256.sha256(a, length)) == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha/packed.sha256(a, length) : Maybe<&2, List<&2, U32>>}

law full_correct unverifiedits file does not pass the checker (fails)source · line 77 · raw

@a:Array<U32> -> @+length:Nat -> {observe(0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/sha256.sha256(a, length)) == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha/packed.sha256(a, length) : Maybe<&2, List<&2, U32>>}

Definitions

def words source · line 29 · raw

@a:Array<U32> -> List<&2, U32>

Proof-only observation; never called by the buffer hashing API.

def observe source · line 43 · raw

@r:Maybe<&1, Array<U32>> -> Maybe<&2, List<&2, U32>>

Full public-result observation against the independent packed specification.