def sif_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32mont.bend:73

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as AQ

73# sub_if32: r < 2 m gives r mod m
74def sif_c(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +r: WU.U64, +hM: {v(m) == 1n+bp : Nat}, +hr: {Nat.is_lt(SW.value(r), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}, +c: Bool, +hc: {X.le(WU.U64{m, 0}, r) == c : Bool}) -> {v(X.sub_if32(r, m, c)) == Nat.mod(SW.value(r), 1n+bp) : Nat}:
75  match c:
76    case True{}:
77      +hmv = Equal.trans(Nat, SW.value(WU.U64{m, 0}), v(m), 1n+bp, M128.val0(m), hM)
78      +hm32 = WW.lt_one(32n, one, h1, 1n+bp, L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, v(m), 1n+bp, hM, LW.vb(m)))
79      +hle0 = Equal.trans(Bool, Nat.is_le(SW.value(WU.U64{m, 0}), SW.value(r)), X.le(WU.U64{m, 0}, r), True{}, Equal.sym(Bool, X.le(WU.U64{m, 0}, r), Nat.is_le(SW.value(WU.U64{m, 0}), SW.value(r)), WA.le_value(WU.U64{m, 0}, r)), hc)
80      +hle = L.subst(Nat, z => {Nat.is_le(z, SW.value(r)) == True{} : Bool}, SW.value(WU.U64{m, 0}), 1n+bp, hmv, hle0)
81      +w = X.sub(r, WU.U64{m, 0})
82      +es = Equal.trans(Nat, SW.value(w), Nat.sub(SW.value(r), SW.value(WU.U64{m, 0})), Nat.sub(SW.value(r), 1n+bp), WA.sub_value(r, WU.U64{m, 0}, hle0), Equal.cong(Nat, Nat, z => Nat.sub(SW.value(r), z), SW.value(WU.U64{m, 0}), 1n+bp, hmv))
83      +x = Nat.sub(SW.value(r), 1n+bp)
84      +hx = N.sub_lt(SW.value(r), 1n+bp, 1n+bp, hle, hr)
85      +f = WW.fits_one(32n, one, h1, SW.value(w), L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, x, SW.value(w), Equal.sym(Nat, SW.value(w), x, es), N.lt_trans(x, 1n+bp, C.shift(32n, one), hx, hm32)))
86      +er = Equal.trans(Nat, Nat.add(Nat.mul(1n, 1n+bp), x), Nat.add(1n+bp, x), SW.value(r), Equal.cong(Nat, Nat, z => Nat.add(z, x), Nat.mul(1n, 1n+bp), 1n+bp, AQ.mul1(1n+bp)), N.sub_add(SW.value(r), 1n+bp, hle))
87      +em = Equal.trans(Nat, Nat.mod(SW.value(r), 1n+bp), Nat.mod(Nat.add(Nat.mul(1n, 1n+bp), x), 1n+bp), x, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), SW.value(r), Nat.add(Nat.mul(1n, 1n+bp), x), Equal.sym(Nat, Nat.add(Nat.mul(1n, 1n+bp), x), SW.value(r), er)), NR.mod_of(1n, bp, x, hx))
88      Equal.trans(Nat, v(X.lo(w)), x, Nat.mod(SW.value(r), 1n+bp), Equal.trans(Nat, v(X.lo(w)), SW.value(w), x, lo32(w, f), es), Equal.sym(Nat, Nat.mod(SW.value(r), 1n+bp), x, em))
89    case False{}:
90      +hmv = Equal.trans(Nat, SW.value(WU.U64{m, 0}), v(m), 1n+bp, M128.val0(m), hM)
91      +hm32 = WW.lt_one(32n, one, h1, 1n+bp, L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, v(m), 1n+bp, hM, LW.vb(m)))
92      +hle0 = Equal.trans(Bool, Nat.is_le(SW.value(WU.U64{m, 0}), SW.value(r)), X.le(WU.U64{m, 0}, r), False{}, Equal.sym(Bool, X.le(WU.U64{m, 0}, r), Nat.is_le(SW.value(WU.U64{m, 0}), SW.value(r)), WA.le_value(WU.U64{m, 0}, r)), hc)
93      +hl = L.subst(Nat, z => {Nat.is_lt(SW.value(r), z) == True{} : Bool}, SW.value(WU.U64{m, 0}), 1n+bp, hmv, N.not_le_lt(SW.value(WU.U64{m, 0}), SW.value(r), hle0))
94      +f = WW.fits_one(32n, one, h1, SW.value(r), N.lt_trans(SW.value(r), 1n+bp, C.shift(32n, one), hl, hm32))
95      Equal.trans(Nat, v(X.lo(r)), SW.value(r), Nat.mod(SW.value(r), 1n+bp), lo32(r, f), Equal.sym(Nat, Nat.mod(SW.value(r), 1n+bp), SW.value(r), NR.mod_of(0n, bp, SW.value(r), hl)))