LAWS.bytes_onto_block16: law of bend-osdev-mode-core@0.1.0.0
Import: import bend-osdev-mode-core@0.1.0.0/LAWS.bend as LAWS
Lines 91-110 of bend-osdev-mode-core@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&start_line=91&end_line=110

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

# the bytes of the block of any 16 values are those values, masked
law bytes_onto_block16:
  for z0: U32
  for z1: U32
  for z2: U32
  for z3: U32
  for z4: U32
  for z5: U32
  for z6: U32
  for z7: U32
  for z8: U32
  for z9: U32
  for z10: U32
  for z11: U32
  for z12: U32
  for z13: U32
  for z14: U32
  for z15: U32
  for rest: List<&2, U32>
  {M.cm.bytes_onto(M.cm.block16(z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15), rest) == Con{B.byte(z0), Con{B.byte(z1), Con{B.byte(z2), Con{B.byte(z3), Con{B.byte(z4), Con{B.byte(z5), Con{B.byte(z6), Con{B.byte(z7), Con{B.byte(z8), Con{B.byte(z9), Con{B.byte(z10), Con{B.byte(z11), Con{B.byte(z12), Con{B.byte(z13), Con{B.byte(z14), Con{B.byte(z15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.blk16g
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.block16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.bytes_onto