law bytes_onto_block16

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:91

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

91# the bytes of the block of any 16 values are those values, masked
92law bytes_onto_block16:
93  for z0: U32
94  for z1: U32
95  for z2: U32
96  for z3: U32
97  for z4: U32
98  for z5: U32
99  for z6: U32
100  for z7: U32
101  for z8: U32
102  for z9: U32
103  for z10: U32
104  for z11: U32
105  for z12: U32
106  for z13: U32
107  for z14: U32
108  for z15: U32
109  for rest: List<&2, U32>
110  {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>}