def clamp_c

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/u32.bend:168

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-crypto@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-crypto@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-crypto@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

168def clamp_c(+x: U32, +lo: U32, +hi: U32, +c: Bool) -> {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp_ok(U32.to_nat(x), U32.to_nat(lo), U32.to_nat(hi), c)) : Result<&2, &2, NM.NumError, U32>}:
169  match c:
170    case True{}:
171      {==}
172    case False{}:
173      %Equal.sym(U32, G.min(~U32, ~I.u32_op, ~I.u32_is, G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo), hi), U32.from_nat(Nat.min(U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)), U32.to_nat(hi))), min_agrees(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo), hi)) : {Done{_} == Done{U32.from_nat(Nat.min(Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(hi)))} : Result<&2, &2, NM.NumError, U32>}
174      %Equal.sym(Nat, U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)), Nat.max(U32.to_nat(x), U32.to_nat(lo)), max_val(x, lo)) : {Done{U32.from_nat(Nat.min(_, U32.to_nat(hi)))} == Done{U32.from_nat(Nat.min(Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(hi)))} : Result<&2, &2, NM.NumError, U32>}
175      {==}