buffer_proof.bend checks

raw source on the hub · import 0x3bdc0c9f5265bb49f7fc76b61f529f24/buffer_proof.bend as Buffer_proof

9 imports

import Base
import ./fips.bend as F
import ./buffer.bend as B
import ./packed.bend as P
import ./packed_spec.bend as R
import ./packed_proof.bend as Proof
import ./packed_array_proof.bend as A
import ./state.bend as S
import ./sha256.bend as SHA

Laws

law correct provedsource · line 11 · raw

@a:Array<U32> -> @+length:Nat -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.sha256(a, length) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/buffer.result(0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_spec.hash(a, length)) : Maybe<&1, Array<U32>>}

law digest_size provedsource · line 20 · raw

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

law digest_words provedsource · line 34 · raw

@+s:0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State -> {words(0x3bdc0c9f5265bb49f7fc76b61f529f24/buffer.digest(s)) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.digest(s) : List<&2, U32>}

law observe_digest provedsource · line 48 · raw

@+r:Maybe<&2, 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.State> -> {observe(0x3bdc0c9f5265bb49f7fc76b61f529f24/buffer.result(r)) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_spec.digest_result(r) : Maybe<&2, List<&2, U32>>}

law full_reified provedsource · line 59 · raw

@-a:Array<U32> -> @+length:Nat -> @view:Sigma<&2, &1, 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_array_proof.Tree, t => {a == 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_array_proof.thaw(t) : Array<U32>}> -> {observe(0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.sha256(a, length)) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_spec.sha256(a, length) : Maybe<&2, List<&2, U32>>}

law full_correct provedsource · line 77 · raw

@a:Array<U32> -> @+length:Nat -> {observe(0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.sha256(a, length)) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_spec.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.