proofs/lib/lemmas/proofs/division_invariant.bend

bend-collections-laws-math@1.0.0.0 · 41 lines · 6 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
3import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound.bend as Candidate
4import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_remainder.bend as Remainder
5import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Logic
6
7def remainder(-n: Nat, result: W.Division<n>) -> U32:
8  W.Div{q, r} = result
9  r
10
11def not_ge(c: Cmp, e: {Cmp.is_ge(c) == False{} : Bool}) -> {Cmp.is_lt(c) == True{} : Bool}:
12  match c:
13    case LT{}: {==}
14    case EQ{}: Empty.absurd({False{} == True{} : Bool}, Logic.false_true(Equal.sym(Bool, True{}, False{}, e)))
15    case GT{}: Empty.absurd({False{} == True{} : Bool}, Logic.false_true(Equal.sym(Bool, True{}, False{}, e)))
16
17# Both branches refer to actual wide.digit_result, not a proof-side divider.
18def result(+p: Nat, q: Word(p), +r: U32, flag: Bool, chosen: {U32.is_ge(r, 1000000) == flag : Bool}, bound: {U32.is_lt(r, 2000000) == True{} : Bool}) -> {U32.is_lt(remainder(1n+p, W.digit_result(p, q, r, flag)), 1000000) == True{} : Bool}:
19  match flag:
20    case False{}:
21      not_ge(U32.cmp(r, 1000000), chosen)
22    case True{}:
23      Remainder.million(r, chosen, bound)
24
25def compare(+p: Nat, +q: Word(p), +r: U32, bound: {U32.is_lt(r, 2000000) == True{} : Bool}) -> {U32.is_lt(remainder(1n+p, W.digit_compare(p, q, r)), 1000000) == True{} : Bool}:
26  result(p, q, r, U32.is_ge(r, 1000000), {==}, bound)
27
28def digit(+p: Nat, +bit: Bool, prior: W.Division<p>, bound: {U32.is_lt(remainder(p, prior), 1000000) == True{} : Bool}) -> {U32.is_lt(remainder(1n+p, W.digit(p, bit, prior)), 1000000) == True{} : Bool}:
29  match prior:
30    case W.Div{q, +r}:
31      compare(p, q, U32.add(U32.mul(r, 2), W.bit_u32(bit)), Candidate.million(r, bit, bound))
32
33# Every recursively reached remainder of the executed divider is strictly below
34# the divisor, for arbitrary widths and inputs. No reachable-range premise.
35def bounded(+n: Nat, word: Word(n)) -> {U32.is_lt(remainder(n, W.div_million(n, word)), 1000000) == True{} : Bool}:
36  match n:
37    case 0n: {==}
38    case 1n+ +p:
39      match word:
40        case WCon{+bit, +tail}:
41          digit(p, bit, W.div_million(p, tail), bounded(p, tail))