def byte_shrn.k

lawful-words@0.1.0.0 · proof_bytes.bend:669

import Base
import lawful-words@0.1.0.0/defs.bend as D

669def byte_shrn.k(+w: U32, +s: Nat, +j: Nat, +k: Nat) ->
670  {D.bit(D.byte(U32.shrn(w, Nat.mul(8n, s)), j), k) == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}:
671  +l = Nat.is_lt(k, 8n)
672  +i = Nat.add(Nat.mul(8n, j), k)
673  %Equal.sym(Bool, D.bit(D.byte(U32.shrn(w, Nat.mul(8n, s)), j), k), Bool.and(l, D.bit(U32.shrn(w, Nat.mul(8n, s)), i)), bit_byte(U32.shrn(w, Nat.mul(8n, s)), j, k)) :
674    {_ == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}
675  %Equal.sym(Bool, D.bit(U32.shrn(w, Nat.mul(8n, s)), i), D.bit(w, Nat.add(i, Nat.mul(8n, s))), bit_shrn(w, Nat.mul(8n, s), i)) :
676    {Bool.and(l, _) == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}
677  %Equal.sym(Bool, D.bit(D.byte(w, Nat.add(j, s)), k), Bool.and(l, D.bit(w, Nat.add(Nat.mul(8n, Nat.add(j, s)), k))), bit_byte(w, Nat.add(j, s), k)) :
678    {Bool.and(l, D.bit(w, Nat.add(i, Nat.mul(8n, s)))) == _ : Bool}
679  %idx_add(j, s, k) : {Bool.and(l, D.bit(w, Nat.add(i, Nat.mul(8n, s)))) == Bool.and(l, D.bit(w, _)) : Bool}
680  {==}