law checked_view

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/proof.bend:62

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/array.bend as A

62law checked_view:
63  for -a: Array<U32>
64  for +length: Nat
65  for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>
66  {K.checked(True{},a,length) == S.checked(True{},a,length) : Maybe<&1,Array<U32>>}