def sign_c

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

import Base
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/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U

139def sign_c(+x: U32, +c: Bool, +hc: {Nat.is_lt(0n, U32.to_nat(x)) == c : Bool}) -> {G.sign_above(~U32, ~I.u32_op, ~I.u32_is, x, c) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}:
140  match c:
141    case True{}:
142      %Equal.sym(Nat, Nat.min(U32.to_nat(x), 1n), 1n, N.min_right(U32.to_nat(x), 1n, pos_ge_one(U32.to_nat(x), hc))) : {1 == U32.from_nat(_) : U32}
143      {==}
144    case False{}:
145      %Equal.sym(Bool, U32.is_lt(x, 0), Nat.is_lt(U32.to_nat(x), 0n), U.is_lt_nat(x, 0)) : {G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, _) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}
146      %Equal.sym(Bool, Nat.is_lt(U32.to_nat(x), 0n), False{}, lt_zero_false(U32.to_nat(x))) : {G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, _) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}
147      %Equal.sym(Nat, Nat.min(U32.to_nat(x), 1n), U32.to_nat(x), N.min_left(U32.to_nat(x), 1n, zero_lt_one(U32.to_nat(x), hc))) : {x == U32.from_nat(_) : U32}
148      Equal.sym(U32, U32.from_nat(U32.to_nat(x)), x, round_trip(x))