Conformance.kr45_correct: law of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend as Conformance
Lines 1216-1236 of bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&start_line=1216&end_line=1236

import Base
import bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend as Runtime
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend as C

law kr45_correct:
  for +q: Nat
  for +x0: U32
  for +x1: U32
  for +x2: U32
  for +x3: U32
  for +x4: U32
  for +x5: U32
  for +x6: U32
  for +x7: U32
  for +x8: U32
  for +x9: U32
  for +x10: U32
  for +x11: U32
  for +x12: U32
  for +x13: U32
  for +x14: U32
  for +x15: U32
  for +s: S.State
  {Runtime.kr45(q, Runtime.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, s) ==
    C.window_rounds(q, Runtime.W{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}, [3600352804, 4094571909, 275423344, 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298], s) : S.State}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend&name=kr46_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend&name=window_rounds
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend&name=ShaWindow
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend&name=kr45
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend&name=small0
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend&name=small1
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/packed/core.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/sha/state.bend&name=State