def dm_fin.t

lawful-words@0.1.0.0 · proof_u32.bend:731

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N
import lawful-words@0.1.0.0/proof_word.bend as W

731# The quotient bit is 1: the remainder becomes 2r + a0 - b.
732def dm_fin.t(+p: Nat, +q: Word(p), +s: Word(32n), +t: Bool, +b: U32, +a0: Bool, +hi: Word(p), +r: Nat, +m: Nat,
733  +hm: {Nat.pow(2n, 32n) == m : Nat}, +g: Bool,
734  +eg: {Bool.or(t, U32.is_ge(U32{s}, b)) == g : Bool},
735  +e1: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == Word.to_nat(p, hi) : Nat},
736  +e2: {Nat.is_lt(r, U32.to_nat(b)) == True{} : Bool},
737  +ep: {Nat.add(Word.to_nat(32n, s), Nat.mul(N.bn(t), m)) == Nat.add(N.bn(a0), Nat.double(r)) : Nat}) ->
738  DMOK(1n+p, Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))), U32.to_nat(b), U32.divmod.go.fin(p, q, U32{s}, b, g)):
739  match t g:
740    case True{} True{}:
741      +bb = U32.to_nat(b)
742      +sv = Word.to_nat(32n, s)
743      +rr = Nat.add(N.bn(a0), Nat.double(r))
744      # 2r + a0 = s + m
745      +er = Equal.trans(Nat, rr, Nat.add(sv, Nat.mul(1n, m)), Nat.add(sv, m), Equal.sym(Nat, Nat.add(sv, Nat.mul(1n, m)), rr, ep),
746        Equal.cong(Nat, Nat, z => Nat.add(sv, z), Nat.mul(1n, m), m, N.add_zero(m)))
747      +hle = N.lt_to_le(bb, rr, %Equal.sym(Nat, rr, Nat.add(sv, m), er) : {Nat.is_lt(bb, _) == True{} : Bool}; N.lt_le_trans(bb, m, Nat.add(sv, m), to_nat_lt.m(b, m, hm), N.le_add_l(m, sv)))
748      +hlt = sub_lt_dbl(rr, bb, W.lt_dbl_bit(r, bb, a0, e2), hle)
749      +ev = Equal.trans(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.sub(Nat.add(sv, m), bb), m), Nat.sub(rr, bb),
750        to_nat_sub.m(U32{s}, b, m, hm),
751        %er : {Nat.mod(Nat.sub(_, bb), m) == Nat.sub(rr, bb) : Nat}
752        N.mod_small(Nat.sub(rr, bb), m, N.lt_trans(Nat.sub(rr, bb), bb, m, hlt, to_nat_lt.m(b, m, hm))))
753      (%Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), bb), _) == Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))) : Nat}
754        divstep1(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, Nat.sub(rr, bb), e1, N.le_sub_add(bb, rr, hle)),
755       %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.is_lt(_, bb) == True{} : Bool}; hlt)
756    case True{} False{}:
757      Empty.absurd(DMOK(1n+p, Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))), U32.to_nat(b), (WCon{False{}, q}, U32{s})), N.true_ne_false(eg))
758    case False{} True{}:
759      +bb = U32.to_nat(b)
760      +sv = Word.to_nat(32n, s)
761      +rr = Nat.add(N.bn(a0), Nat.double(r))
762      +er = Equal.trans(Nat, rr, Nat.add(sv, 0n), sv, Equal.sym(Nat, Nat.add(sv, 0n), rr, ep), N.add_zero(sv))
763      +hle = {%Equal.sym(Nat, rr, sv, er) : {Nat.is_le(bb, _) == True{} : Bool}; %ge_le(sv, bb) : {_ == True{} : Bool}; %is_ge_to_nat(U32{s}, b) : {_ == True{} : Bool}; eg :
764        {Nat.is_le(bb, rr) == True{} : Bool}}
765      +hlt = sub_lt_dbl(rr, bb, W.lt_dbl_bit(r, bb, a0, e2), hle)
766      +ev = Equal.trans(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.sub(Nat.add(sv, m), bb), m), Nat.sub(rr, bb),
767        to_nat_sub.m(U32{s}, b, m, hm),
768        %Equal.sym(Nat, rr, sv, er) : {Nat.mod(Nat.sub(Nat.add(sv, m), bb), m) == Nat.sub(_, bb) : Nat}
769        %Equal.sym(Nat, Nat.sub(Nat.add(sv, m), bb), Nat.add(Nat.sub(sv, bb), m), sub_add_comm(sv, m, bb, %er : {Nat.is_le(bb, _) == True{} : Bool}; hle)) :
770          {Nat.mod(_, m) == Nat.sub(sv, bb) : Nat}
771        %Equal.sym(Nat, Nat.mod(Nat.add(Nat.sub(sv, bb), m), m), Nat.mod(Nat.sub(sv, bb), m), mod_add_self(Nat.sub(sv, bb), m)) : {_ == Nat.sub(sv, bb) : Nat}
772        N.mod_small(Nat.sub(sv, bb), m, N.le_lt_trans(Nat.sub(sv, bb), sv, m, sub_le(sv, bb), wlt.m(s, m, hm))))
773      (%Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), bb), _) == Nat.add(N.bn(a0), Nat.double(Word.to_nat(p, hi))) : Nat}
774        divstep1(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, Nat.sub(rr, bb), e1, N.le_sub_add(bb, rr, hle)),
775       %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(rr, bb), ev) : {Nat.is_lt(_, bb) == True{} : Bool}; hlt)
776    case False{} False{}:
777      +bb = U32.to_nat(b)
778      +sv = Word.to_nat(32n, s)
779      +er = Equal.trans(Nat, sv, Nat.add(sv, 0n), Nat.add(N.bn(a0), Nat.double(r)), Equal.sym(Nat, Nat.add(sv, 0n), sv, N.add_zero(sv)), ep)
780      +hlt = N.not_le_lt(bb, sv, %ge_le(sv, bb) : {_ == False{} : Bool}; %is_ge_to_nat(U32{s}, b) : {_ == False{} : Bool}; eg)
781      (divstep0(Word.to_nat(p, q), bb, r, Word.to_nat(p, hi), a0, sv, e1, er), hlt)