law e_hi

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:253

import Base
import lawful-words@0.1.0.0/defs.bend as W
import lawful-bytes@0.1.1.0/fast.bend as FA

253# A byte of the first word at or above the start: the test of c.
254law e_hi:
255  for +w: U32
256  for +c: U32
257  for +m: U32
258  for +j: Nat
259  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
260  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
261  for +hm: {W.byte(m, j) == 0 : U32}
262  {U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), m), j), 0) == U32.is_eq(W.byte(w, j), c) : Bool}