Loop.fuse_step2: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as Loop Lines 92-112 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&start_line=92&end_line=112 import Base import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T 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 import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/chunk.bend as CH import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend as TR def fuse_step2(+p: Nat, +t: U32, +index: U32, +len: Nat, +s: K.Stack, -a: Array, +o: T.Out, view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array}>, rec: @a2: Array -> @s2: K.Stack -> {K.chunks(p,U32.inc(t),U32.add(index,256),len,(a2,s2)) == run(s2,S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,a2))) : T.Out} ) -> {K.chunks(p,U32.inc(t),U32.add(index,256),len,K.pushed(s,CH.outcv((a,o)))) == run(s,S.chunks(1n+p,t,index,len,(a,o))) : T.Out}: match view: case Tuple{+tree,pf}: %Equal.sym(Array,a,A.thaw(tree),pf) : {K.chunks(p,U32.inc(t),U32.add(index,256),len,K.pushed(s,CH.outcv((_,o)))) == run(s,S.chunks(1n+p,t,index,len,(_,o))) : T.Out} Equal.trans(T.Out, K.chunks(p,U32.inc(t),U32.add(index,256),len,(A.thaw(tree),K.push(s,S.cv(o)))), run(K.push(s,S.cv(o)),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))), run2(S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree))),s,o), rec(A.thaw(tree),K.push(s,S.cv(o))), Equal.trans(T.Out, run(K.push(s,S.cv(o)),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))), run(K.push(s,K.out_cv(o)),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))), run2(S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree))),s,o), Equal.cong(T.CV,T.Out,c => run(K.push(s,c),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))), S.cv(o),K.out_cv(o),Equal.sym(T.CV,K.out_cv(o),S.cv(o),TR.out_cv_correct(o))), Equal.sym(T.Out,run2(S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree))),s,o), run(K.push(s,K.out_cv(o)),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))), run2_run(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)),s,o)))) Uses (26): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.inc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/array.bend&name=Tree https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/array.bend&name=thaw https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/chunk.bend&name=outcv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=run https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=run2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=run2_run https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=out_cv_correct https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=chunk_at https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=chunks https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=cv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=Stack https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=chunks https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=out_cv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=push https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=pushed https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=CV https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=Out