proofs/lib/lemmas/proofs/division_candidate.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend as Division_candidate

7 imports

import Base
import ./word_comparison.bend as Comparison
import ../src/wide.bend as W
import ../spec/numeric.bend as S
import ./word_multiplication.bend as Mul
import ./word_shift.bend as Shift
import ./numeric.bend as N

Definitions

def times_two source · line 9 · raw

@a:Nat -> {Nat.mul(a, 2n) == Nat.double(a) : Nat}

def doubling source · line 16 · raw

@+r:U32 -> {U32.mul(r, 2) == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(32n, Nat.double(U32.to_nat(r)))} : U32}

The actual U32 multiplication in wide.digit computes low bits of 2*r.

def shift_value source · line 19 · raw

@r:U32 -> {U32.shl(r) == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(32n, Nat.double(U32.to_nat(r)))} : U32}

def multiplication_is_shift source · line 24 · raw

@+r:U32 -> {U32.mul(r, 2) == U32.shl(r) : U32}

def digit source · line 29 · raw

@+p:Nat -> @+bit:Bool -> @+q:Word(p) -> @+r:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.digit(p, bit, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.Div{q, r}) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.digit_compare(p, q, U32.add(U32.shl(r), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.bit_u32(bit))) : 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.Division<1n+p>}

Link directly to the recurrence used by actual div_million. This equation is still modular; the reachable remainder range must be discharged separately.