def fixz

bend-osdev-gf@0.1.1.0 · PROOF.bend:1875

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

1875# a nonzero byte as itself, and 0 as 1, so that the per-byte facts hold
1876# for every byte and need no hypothesis while they are split into cases
1877def fixz(+x: U32) -> U32:
1878  Bool.pick(U32, G.Gf8.is_zero(x), 1, x)