bend-collections-laws-math Releases (1): 1.0.0.0 0xf86f5f1d9a594d5a5cff999100e01d03 indexed https://jend.leeeet.dev/files.txt?path=bend-collections-laws-math@1.0.0.0 Definitions (5526, 1 to 100 shown): Arith.sc (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc) def sc(+n: Nat, +k: Nat) -> Nat: Arith.mul_sc (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=mul_sc) def mul_sc(+k: Nat, +x: Nat) -> {Nat.mul(x, sc(k, 1n)) == sc(k, x) : Nat}: Arith.mul_sc1 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=mul_sc1) def mul_sc1(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {Nat.mul(x, sc(k, one)) == sc(k, x) : Nat}: Arith.sc_mul (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_mul) def sc_mul(+k: Nat, +q: Nat, +d: Nat) -> {sc(k, Nat.mul(q, d)) == Nat.mul(sc(k, q), d) : Nat}: Arith.sc_le (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_le) def sc_le(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(sc(k, a), sc(k, b)) == True{} : Bool}: Arith.sc_lt (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_lt) def sc_lt(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(sc(k, a), sc(k, b)) == True{} : Bool}: Arith.sc_lt_cancel_g (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_lt_cancel_g) def sc_lt_cancel_g(+k: Nat, +a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}, +h: {Nat.is_lt(sc(k, a), sc(k, b)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}: Arith.sc_lt_cancel (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_lt_cancel) def sc_lt_cancel(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(sc(k, a), sc(k, b)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}: Arith.le_sc (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=le_sc) def le_sc(+k: Nat, +x: Nat) -> {Nat.is_le(x, sc(k, x)) == True{} : Bool}: Arith.digit_lt (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=digit_lt) # a digit x below 2^k after y < b scaled by 2^k stays below b scaled def digit_lt(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +b: Nat, +hx: {Nat.is_lt(x, sc(k, one)) == True{} : Bool}, +hy: {Nat.is_lt(y, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(sc(k, y), x), sc(k, b)) == True{} : Bool}: Arith.mul_le (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=mul_le) def mul_le(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}: Arith.one_mul (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=one_mul) def one_mul(+d: Nat) -> {Nat.mul(1n, d) == d : Nat}: Arith.quot_lt_g (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=quot_lt_g) def quot_lt_g(+k: Nat, +q: Nat, +d: Nat, +r: Nat, +c: Bool, +hc: {Nat.is_lt(q, sc(k, 1n)) == c : Bool}, +h: {Nat.is_lt(Nat.add(Nat.mul(q, d), r), sc(k, d)) == True{} : Bool}) -> {Nat.is_lt(q, sc(k, 1n)) == True{} : Bool}: Arith.quot_lt (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=quot_lt) # q d + r < 2^k d forces q < 2^k def quot_lt(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +d: Nat, +r: Nat, +h: {Nat.is_lt(Nat.add(Nat.mul(q, d), r), sc(k, d)) == True{} : Bool}) -> {Nat.is_lt(q, sc(k, one)) == True{} : Bool}: Arith.step (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=step) # one long-division step: if x == q d + r and 2^k r + y == q2 d + r2 then # 2^k x + y == (2^k q + q2) d + r2 def step(+k: Nat, +q: Nat, +r: Nat, +d: Nat, +y: Nat, +q2: Nat, +r2: Nat, +x: Nat, +hx: {x == Nat.add(Nat.mul(q, d), r) : Nat}, +h2: {Nat.add(sc(k, r), y) == Nat.add(Nat.mul(q2, d), r2) : Nat}) -> {Nat.add(sc(k, x), y) == Nat.add(Nat.mul(Nat.add(sc(k, q), q2), d), r2) : Nat}: Arith.go_le (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=go_le) def go_le(+n: Nat, +m: Nat, +d: Nat, +r: Nat) -> {Nat.is_le(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), Nat.add(d, n)) == True{} : Bool}: Arith.div_le (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=div_le) # a quotient never exceeds its dividend def div_le(+a: Nat, +d: Nat) -> {Nat.is_le(Nat.div(a, d), a) == True{} : Bool}: Arith.zsub (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=zsub) def zsub(+b: Nat) -> {Nat.sub(0n, b) == 0n : Nat}: Arith.sub_cancel_l (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sub_cancel_l) def sub_cancel_l(+c: Nat, +a: Nat, +b: Nat) -> {Nat.sub(Nat.add(c, a), Nat.add(c, b)) == Nat.sub(a, b) : Nat}: Arith.sc_idx (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_idx) # 2^(k + j) x == 2^k (2^j x) def sc_idx(+k: Nat, +j: Nat, +x: Nat) -> {sc(Nat.add(k, j), x) == sc(k, sc(j, x)) : Nat}: Arith.sc_sub (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sc_sub) # 2^k (a - b) == 2^k a - 2^k b def sc_sub(+k: Nat, +a: Nat, +b: Nat) -> {sc(k, Nat.sub(a, b)) == Nat.sub(sc(k, a), sc(k, b)) : Nat}: Arith.sub_le2 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend&name=sub_le2) # a - b <= a def sub_le2(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}: Addition.sum_bit (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=sum_bit) # Carry is computed from input bits; it is not an assumed property of Word.add. def sum_bit(r: Bool & Bool) -> Bool: Addition.carry_bit (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=carry_bit) def carry_bit(r: Bool & Bool) -> Bool: Addition.carry_out (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=carry_out) def carry_out(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool: Addition.bit_conservation (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=bit_conservation) law bit_conservation: for a: Nat for +b: Nat for x: Bool for y: Bool for c: Bool {Nat.add(S.bit_value(sum_bit(Bool.full_add(x, y, c))), Nat.double(Nat.add(S.bit_value(carry_bit(Bool.full_add(x, y, c))), Nat.add(a, b)))) == Nat.add(S.bit_value(c), Nat.add(Nat.add(S.bit_value(x), Nat.double(a)), Nat.add(S.bit_value(y), Nat.double(b)))) : Nat} Addition.lift_conservation (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=lift_conservation) law lift_conservation: for +bit: Bool for +value: Nat for +carry: Nat for +total: Nat for e: {Nat.add(value, carry) == total : Nat} {Nat.add(Nat.add(S.bit_value(bit), Nat.double(value)), Nat.double(carry)) == Nat.add(S.bit_value(bit), Nat.double(total)) : Nat} Addition.adc_shape (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=adc_shape) law adc_shape: for +n: Nat for a: Word(n) for b: Word(n) for pair: Bool & Bool {Word.adc.con(n, a, b, False{}, pair) == WCon{sum_bit(pair), Word.adc(n, a, b, False{}, carry_bit(pair))} : Word(1n+n)} Addition.step (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=step) law step: for +n: Nat for +a: Word(n) for +b: Word(n) for +x: Bool for +y: Bool for +c: Bool for e: {Nat.add(S.unsigned(n, Word.adc(n, a, b, False{}, carry_bit(Bool.full_add(x, y, c)))), S.scale_binary(n, S.bit_value(carry_out(n, a, b, carry_bit(Bool.full_add(x, y, c)))))) == Nat.add(S.bit_value(carry_bit(Bool.full_add(x, y, c))), Nat.add(S.unsigned(n, a), S.unsigned(n, b))) : Nat} {Nat.add(S.unsigned(1n+n, Word.adc(1n+n, WCon{x, a}, WCon{y, b}, False{}, c)), S.scale_binary(1n+n, S.bit_value(carry_out(1n+n, WCon{x, a}, WCon{y, b}, c)))) == Nat.add(S.bit_value(c), Nat.add(S.unsigned(1n+n, WCon{x, a}), S.unsigned(1n+n, WCon{y, b}))) : Nat} Addition.adc_conservation (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=adc_conservation) law adc_conservation: for +n: Nat for a: Word(n) for b: Word(n) for +c: Bool {Nat.add(S.unsigned(n, Word.adc(n, a, b, False{}, c)), S.scale_binary(n, S.bit_value(carry_out(n, a, b, c)))) == Nat.add(S.bit_value(c), Nat.add(S.unsigned(n, a), S.unsigned(n, b))) : Nat} Addition.addition_conservation (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend&name=addition_conservation) # A full-width arithmetic law linked to the actual cache deadline adder. # Range/modulo uniqueness and signed division are separate remaining obligations. law addition_conservation: for +a: Word(64n) for +b: Word(64n) {Nat.add(S.unsigned(64n, W.add(a, b)), S.scale_binary(64n, S.bit_value(carry_out(64n, a, b, False{})))) == Nat.add(S.unsigned(64n, a), S.unsigned(64n, b)) : Nat} AdditionBounds.offset_not_less (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend&name=offset_not_less) def offset_not_less(b: Nat, +a: Nat) -> {Nat.is_lt(Nat.add(a, b), b) == False{} : Bool}: AdditionBounds.no_wrap (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend&name=no_wrap) # Input range discharges the carry, rather than assuming no overflow. def no_wrap(+n: Nat, +result: Nat, +total: Nat, carry: Bool, conservation: {Nat.add(result, S.scale_binary(n, S.bit_value(carry))) == total : Nat}, bound: {Nat.is_lt(total, S.scale_binary(n, 1n)) == True{} : Bool}) -> {result == total : Nat}: AdditionBounds.exact (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend&name=exact) def exact(+n: Nat, +a: Word(n), +b: Word(n), bound: {Nat.is_lt(Nat.add(S.unsigned(n, a), S.unsigned(n, b)), S.scale_binary(n, 1n)) == True{} : Bool}) -> {S.unsigned(n, Word.add(n, a, b)) == Nat.add(S.unsigned(n, a), S.unsigned(n, b)) : Nat}: Counter.carry (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend&name=carry) # Carry out is mathematical all-bits-set, not an assumed increment result. def carry(n: Nat, w: Word(n)) -> Bool: Counter.scale_zero (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend&name=scale_zero) law scale_zero: for n: Nat {S.scale_binary(n, 0n) == 0n : Nat} Counter.increment_conservation (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend&name=increment_conservation) # Exact integer conservation for the installed ripple increment at every width: # result + (carry-out * 2^width) = input + 1. This includes width zero and proves # all bit patterns, rather than testing only the maximum-word rollover example. law increment_conservation: for +n: Nat for w: Word(n) {Nat.add(S.unsigned(n, Word.inc(n, w)), S.scale_binary(n, S.bit_value(carry(n, w)))) == 1n+S.unsigned(n, w) : Nat} Counter.counter_conservation (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend&name=counter_conservation) law counter_conservation: for +w: Word(64n) {Nat.add(S.unsigned(64n, W.inc(w)), S.scale_binary(64n, S.bit_value(carry(64n, w)))) == 1n+S.unsigned(64n, w) : Nat} DivisionBounds.candidate (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend&name=candidate) # A long-division candidate is less than twice the divisor for either input bit. def candidate(+r: Nat, +d: Nat, +bit: Bool, bound: {Nat.is_lt(r, d) == True{} : Bool}) -> {Nat.is_lt(Nat.add(S.bit_value(bit), Nat.double(r)), Nat.double(d)) == True{} : Bool}: DivisionBounds.cancel_less (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend&name=cancel_less) def cancel_less(a: Nat, +b: Nat, +c: Nat) -> {Nat.is_lt(Nat.add(a, b), Nat.add(a, c)) == Nat.is_lt(b, c) : Bool}: DivisionBounds.ge_reverse (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend&name=ge_reverse) def ge_reverse(a: Nat, b: Nat) -> {Nat.is_ge(a, b) == Nat.is_le(b, a) : Bool}: DivisionBounds.not_ge (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend&name=not_ge) def not_ge(a: Nat, b: Nat, e: {Nat.is_ge(a, b) == False{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}: DivisionBounds.subtract_bound (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend&name=subtract_bound) # Subtracting the divisor once restores the strict remainder bound. def subtract_bound(+r: Nat, +d: Nat, inside: {Nat.is_lt(r, Nat.add(d, d)) == True{} : Bool}, enough: {Nat.is_le(d, r) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(r, d), d) == True{} : Bool}: DivisionCandidate.times_two (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend&name=times_two) def times_two(a: Nat) -> {Nat.mul(a, 2n) == Nat.double(a) : Nat}: DivisionCandidate.doubling (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend&name=doubling) # The actual U32 multiplication in wide.digit computes low bits of 2*r. def doubling(+r: U32) -> {U32.mul(r, 2) == U32{S.from_nat(32n, Nat.double(U32.to_nat(r)))} : U32}: DivisionCandidate.shift_value (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend&name=shift_value) def shift_value(r: U32) -> {U32.shl(r) == U32{S.from_nat(32n, Nat.double(U32.to_nat(r)))} : U32}: DivisionCandidate.multiplication_is_shift (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend&name=multiplication_is_shift) def multiplication_is_shift(+r: U32) -> {U32.mul(r, 2) == U32.shl(r) : U32}: DivisionCandidate.digit (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend&name=digit) # Link directly to the recurrence used by actual div_million. This equation is # still modular; the reachable remainder range must be discharged separately. def digit(+p: Nat, +bit: Bool, +q: Word(p), +r: U32) -> {W.digit(p, bit, W.Div{q, r}) == W.digit_compare(p, q, U32.add(U32.shl(r), W.bit_u32(bit))) : W.Division<1n+p>}: DivisionCandidateBound.lt_le (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound.bend&name=lt_le) def lt_le(c: Cmp, e: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_le(c) == True{} : Bool}: DivisionCandidateBound.smaller_high (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound.bend&name=smaller_high) def smaller_high(r: U32, d: U32, high: {W.last(32n, Overflow.bits(d)) == False{} : Bool}, less: {U32.is_lt(r, d) == True{} : Bool}) -> {W.last(32n, Overflow.bits(r)) == False{} : Bool}: DivisionCandidateBound.native (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound.bend&name=native) def native(+r: U32, +d: U32, +bit: Bool, +high: {W.last(32n, Overflow.bits(d)) == False{} : Bool}, +less: {U32.is_lt(r, d) == True{} : Bool}) -> {U32.is_lt(U32.add(U32.mul(r, 2), W.bit_u32(bit)), U32.shl(d)) == True{} : Bool}: DivisionCandidateBound.million (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound.bend&name=million) def million(+r: U32, +bit: Bool, less: {U32.is_lt(r, 1000000) == True{} : Bool}) -> {U32.is_lt(U32.add(U32.mul(r, 2), W.bit_u32(bit)), 2000000) == True{} : Bool}: DivisionInvariant.remainder (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend&name=remainder) def remainder(-n: Nat, result: W.Division) -> U32: DivisionInvariant.not_ge (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend&name=not_ge) def not_ge(c: Cmp, e: {Cmp.is_ge(c) == False{} : Bool}) -> {Cmp.is_lt(c) == True{} : Bool}: DivisionInvariant.result (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend&name=result) # Both branches refer to actual wide.digit_result, not a proof-side divider. def 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}: DivisionInvariant.compare (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend&name=compare) def 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}: DivisionInvariant.digit (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend&name=digit) def digit(+p: Nat, +bit: Bool, prior: W.Division

, bound: {U32.is_lt(remainder(p, prior), 1000000) == True{} : Bool}) -> {U32.is_lt(remainder(1n+p, W.digit(p, bit, prior)), 1000000) == True{} : Bool}: DivisionInvariant.bounded (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend&name=bounded) # Every recursively reached remainder of the executed divider is strictly below # the divisor, for arbitrary widths and inputs. No reachable-range premise. def bounded(+n: Nat, word: Word(n)) -> {U32.is_lt(remainder(n, W.div_million(n, word)), 1000000) == True{} : Bool}: DivisionNoOverflow.higher_le (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=higher_le) # Higher-bit comparison cannot be greater if the complete comparison is <=. def higher_le(c: Cmp, x: Bool, y: Bool, e: {Cmp.is_le(Word.cmp.fin(x, y, c)) == True{} : Bool}) -> {Cmp.is_le(c) == True{} : Bool}: DivisionNoOverflow.high_monotone (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=high_monotone) def high_monotone(n: Nat, a: Word(1n+n), b: Word(1n+n), low: {W.last(1n+n, b) == False{} : Bool}, le: {Cmp.is_le(Word.cmp(1n+n, a, b)) == True{} : Bool}) -> {W.last(1n+n, a) == False{} : Bool}: DivisionNoOverflow.discarded (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=discarded) def discarded(n: Nat, input: Bool, w: Word(1n+n)) -> {Shift.carry(1n+n, input, w) == W.last(1n+n, w) : Bool}: DivisionNoOverflow.bits (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=bits) def bits(x: U32) -> Word(32n): DivisionNoOverflow.bounded_carry (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=bounded_carry) # The concrete divisor is handled as a native 32-bit word, avoiding expansion # of a million unary constructors. This establishes absence of carry from the # actual U32 comparison premise, not an assumed resource/range conclusion. def bounded_carry(+w: Word(32n), +bit: Bool, le: {U32.is_le(U32{w}, 1000000) == True{} : Bool}) -> {Shift.carry(32n, bit, w) == False{} : Bool}: DivisionNoOverflow.exact_without_carry (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=exact_without_carry) def exact_without_carry(+n: Nat, +w: Word(n), +bit: Bool, no_carry: {Shift.carry(n, bit, w) == False{} : Bool}) -> {S.unsigned(n, Word.shl.put(n, bit, w)) == Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))) : Nat}: DivisionNoOverflow.decoded_candidate (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=decoded_candidate) def decoded_candidate(+w: Word(32n), +bit: Bool, le: {U32.is_le(U32{w}, 1000000) == True{} : Bool}) -> {Word.to_nat(32n, Word.shl.put(32n, bit, w)) == Nat.add(S.bit_value(bit), Nat.double(Word.to_nat(32n, w))) : Nat}: DivisionNoOverflow.candidate_value (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=candidate_value) def candidate_value(+r: U32, +bit: Bool, le: {U32.is_le(r, 1000000) == True{} : Bool}) -> {U32.to_nat(U32.add(U32.mul(r, 2), W.bit_u32(bit))) == Nat.add(S.bit_value(bit), Nat.double(U32.to_nat(r))) : Nat}: DivisionNoOverflow.decoded_high (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=decoded_high) def decoded_high(+w: Word(32n), +bit: Bool, high: {W.last(32n, w) == False{} : Bool}) -> {Word.to_nat(32n, Word.shl.put(32n, bit, w)) == Nat.add(S.bit_value(bit), Nat.double(Word.to_nat(32n, w))) : Nat}: DivisionNoOverflow.double_value (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=double_value) def double_value(d: U32, high: {W.last(32n, bits(d)) == False{} : Bool}) -> {U32.to_nat(U32.shl(d)) == Nat.double(U32.to_nat(d)) : Nat}: DivisionNoOverflow.high_candidate (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend&name=high_candidate) def high_candidate(+r: U32, +bit: Bool, high: {W.last(32n, bits(r)) == False{} : Bool}) -> {U32.to_nat(U32.add(U32.mul(r, 2), W.bit_u32(bit))) == Nat.add(S.bit_value(bit), Nat.double(U32.to_nat(r))) : Nat}: DivisionQuotient.below_successor (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=below_successor) def below_successor(r: Nat, p: Nat) -> {Nat.is_lt(r, 1n+p) == Nat.is_le(r, p) : Bool}: DivisionQuotient.identify (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=identify) def identify(+q: Nat, d: Nat, +r: Nat, bound: {Nat.is_lt(r, d) == True{} : Bool}) -> {Nat.div(Nat.add(Nat.mul(q, d), r), d) == q : Nat}: DivisionQuotient.quotient (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=quotient) def quotient(-n: Nat, result: W.Division) -> Word(n): DivisionQuotient.recognizes (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=recognizes) def recognizes(+n: Nat, result: W.Division, +d: U32, bound: {U32.is_lt(Inv.remainder(n, result), d) == True{} : Bool}) -> {Nat.div(Value.value(n, result, d), U32.to_nat(d)) == S.unsigned(n, quotient(n, result)) : Nat}: DivisionQuotient.natural_quotient (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=natural_quotient) def natural_quotient(+n: Nat, +word: Word(n), +d: U32, +same: {d == 1000000 : U32}) -> {Nat.div(S.unsigned(n, word), U32.to_nat(d)) == S.unsigned(n, quotient(n, W.div_million(n, word))) : Nat}: DivisionQuotient.reconstruct (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=reconstruct) def reconstruct(+n: Nat, +word: Word(n)) -> {S.from_nat(n, S.unsigned(n, word)) == word : Word(n)}: DivisionQuotient.word_quotient (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=word_quotient) def word_quotient(+n: Nat, +word: Word(n), +d: U32, same: {d == 1000000 : U32}) -> {quotient(n, W.div_million(n, word)) == S.from_nat(n, Nat.div(S.unsigned(n, word), U32.to_nat(d))) : Word(n)}: DivisionQuotient.specification_equation (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=specification_equation) def specification_equation(+n: Nat, word: Word(n), +d: U32) -> {Spec.quotient(n, word, d) == S.from_nat(n, Nat.div(S.unsigned(n, word), U32.to_nat(d))) : Word(n)}: DivisionQuotient.guarded (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=guarded) def guarded(+n: Nat, +word: Word(n), +d: U32, same: {d == 1000000 : U32}) -> {quotient(n, W.div_million(n, word)) == Spec.quotient(n, word, d) : Word(n)}: DivisionQuotient.actual (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=actual) def actual(+n: Nat, word: Word(n)) -> {quotient(n, W.div_million(n, word)) == Spec.quotient(n, word, 1000000) : Word(n)}: DivisionQuotient.native_projection (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=native_projection) def native_projection(result: W.Division<64n>) -> {W.quotient(result) == quotient(64n, result) : Word(64n)}: DivisionQuotient.unsigned_milliseconds (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend&name=unsigned_milliseconds) # Connection to the actual duration core and the public independent numeric # specification's nonnegative branch. Negative sign handling is separate. def unsigned_milliseconds(+word: Word(64n)) -> {W.unsigned_milliseconds(word) == S.quotient_signed(word, False{}) : Word(64n)}: DivisionRemainder.subtract (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_remainder.bend&name=subtract) # General U32 subtraction branch; comparison and decoded subtraction are both # justified by the actual Base definitions, and the input range is explicit. def subtract(+r: U32, +d: U32, above: {U32.is_ge(r, d) == True{} : Bool}, below: {Nat.is_lt(U32.to_nat(r), Nat.double(U32.to_nat(d))) == True{} : Bool}) -> {U32.is_lt(U32.sub(r, d), d) == True{} : Bool}: DivisionRemainder.subtract_native (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_remainder.bend&name=subtract_native) def subtract_native(+r: U32, +d: U32, high: {W.last(32n, Overflow.bits(d)) == False{} : Bool}, above: {U32.is_ge(r, d) == True{} : Bool}, below: {U32.is_lt(r, U32.shl(d)) == True{} : Bool}) -> {U32.is_lt(U32.sub(r, d), d) == True{} : Bool}: DivisionRemainder.million (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_remainder.bend&name=million) # Concrete executed subtraction restores the native remainder bound. def million(+r: U32, above: {U32.is_ge(r, 1000000) == True{} : Bool}, below: {U32.is_lt(r, 2000000) == True{} : Bool}) -> {U32.is_lt(U32.sub(r, 1000000), 1000000) == True{} : Bool}: DivisionRemainder.subtraction_conservation (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_remainder.bend&name=subtraction_conservation) def subtraction_conservation(+r: U32, +d: U32, above: {U32.is_ge(r, d) == True{} : Bool}) -> {U32.to_nat(r) == Nat.add(U32.to_nat(d), U32.to_nat(U32.sub(r, d))) : Nat}: DivisionShift.add_zero (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend&name=add_zero) # Adding the incoming bit to an even shifted word changes only its low bit. def add_zero(+n: Nat, w: Word(n)) -> {Word.add(n, w, Word.zero(n)) == w : Word(n)}: DivisionShift.bit_word (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend&name=bit_word) def bit_word(n: Nat, bit: Bool) -> Word(n): DivisionShift.add_bit (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend&name=add_bit) def add_bit(+n: Nat, +w: Word(n), bit: Bool) -> {Word.add(n, Word.shl(n, w), bit_word(n, bit)) == Word.shl.put(n, bit, w) : Word(n)}: DivisionShift.primitive_bit (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend&name=primitive_bit) def primitive_bit(bit: Bool) -> {W.bit_u32(bit) == U32{bit_word(32n, bit)} : U32}: DivisionShift.shifted (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend&name=shifted) def shifted(r: U32, bit: Bool) -> U32: DivisionShift.actual_candidate (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend&name=actual_candidate) # This is the exact candidate expression executed in wide.digit. def actual_candidate(+r: U32, +bit: Bool) -> {U32.add(U32.mul(r, 2), W.bit_u32(bit)) == shifted(r, bit) : U32}: DivisionShift.exact (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend&name=exact) # The range premise concerns the inputs and discharges discarded carry. def exact(+n: Nat, +w: Word(n), +bit: Bool, bound: {Nat.is_lt(Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))), S.scale_binary(n, 1n)) == True{} : Bool}) -> {S.unsigned(n, Word.shl.put(n, bit, w)) == Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))) : Nat}: DivisionValue.value (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=value) # A mathematical observation of the actual returned quotient and remainder. def value(+n: Nat, result: W.Division, d: U32) -> Nat: DivisionValue.selected (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=selected) def selected(+r: U32, d: U32, flag: Bool) -> U32: DivisionValue.selection_value (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=selection_value) def selection_value(+r: U32, +d: U32, flag: Bool, chosen: {U32.is_ge(r, d) == flag : Bool}) -> {U32.to_nat(r) == Nat.add(Nat.mul(S.bit_value(flag), U32.to_nat(d)), U32.to_nat(selected(r, d, flag))) : Nat}: DivisionValue.result_form (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=result_form) # Normal form of the actual helper; the denominator identity is explicit. def result_form(+p: Nat, +q: Word(p), +r: U32, +d: U32, flag: Bool, same: {d == 1000000 : U32}) -> {W.digit_result(p, q, r, flag) == W.Div{WCon{flag, q}, selected(r, d, flag)} : W.Division<1n+p>}: DivisionValue.weight_step (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=weight_step) def weight_step(+q: Nat, +d: Nat, +r: Nat, flag: Bool) -> {Nat.add(Nat.mul(Nat.add(S.bit_value(flag), Nat.double(q)), d), r) == Nat.add(Nat.mul(Nat.double(q), d), Nat.add(Nat.mul(S.bit_value(flag), d), r)) : Nat}: DivisionValue.result_value (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=result_value) def result_value(+p: Nat, +q: Word(p), +r: U32, +d: U32, +flag: Bool, +same: {d == 1000000 : U32}, chosen: {U32.is_ge(r, 1000000) == flag : Bool}) -> {value(1n+p, W.digit_result(p, q, r, flag), d) == Nat.add(Nat.mul(Nat.double(S.unsigned(p, q)), U32.to_nat(d)), U32.to_nat(r)) : Nat}: DivisionValue.gather (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=gather) def gather(+q: Nat, +r: Nat, bit: Bool) -> {Nat.add(Nat.double(q), Nat.add(S.bit_value(bit), Nat.double(r))) == Nat.add(S.bit_value(bit), Nat.double(Nat.add(q, r))) : Nat}: DivisionValue.digit (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend&name=digit) def digit(+p: Nat, +bit: Bool, prior: W.Division

, +d: U32, same: {d == 1000000 : U32}, bound: {U32.is_lt(Inv.remainder(p, prior), 1000000) == True{} : Bool}) -> {value(1n+p, W.digit(p, bit, prior), d) == Nat.add(S.bit_value(bit), Nat.double(value(p, prior, d))) : Nat}: More: https://jend.leeeet.dev/packages/bend-collections-laws-math.txt?definitions_offset=100