def jam
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as W64import Base
112# shifted right, with the shifted-out bits OR-ed into bit 0 (SoftFloat's
113# softfloat_shiftRightJam64); jam(q, r) sets q's bit 0 when r is nonzero
114def jam(+q: Nat, +r: Nat) -> Nat:
115 Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(Nat.mod(q, 2n), Nat.min(r, 1n)))
Uses (7)
Used by (9)
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh:jam_r1
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh:huge_n
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh:jam0_m
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh:jam1_k
- bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh:jam1_m
- …