Compress.diagonal3_correct: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/compress.bend as Compress
Lines 203-213 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/compress.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/compress.bend&start_line=203&end_line=213

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/compress.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as S

law diagonal3_correct:
  for +v: T.State
  for +x0: T.Lane
  for +x1: T.Lane
  for +x2: T.Lane
  for +x3: T.Lane
  for +x4: T.Lane
  for +x5: T.Lane
  for +x6: T.Lane
  for +x7: T.Lane
  {I.diagonal3(v,x0,x1,x2,x3,x4,x5,x6,x7) == S.G(S.G(S.G(S.G(v,0n,5n,10n,15n,x0,x1),1n,6n,11n,12n,x2,x3),2n,7n,8n,13n,x4,x5),3n,4n,9n,14n,x6,x7) : T.State}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend&name=G
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/compress.bend&name=diagonal3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=Lane
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=State