proofs/lib/lemmas/proofs/modular_addition.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as Modular_addition
10 imports
import Base import ../spec/numeric.bend as S import ../src/wide.bend as W import ../src/time.bend as Time import ../types/model.bend as T import ./addition.bend as Add import ./counter.bend as Counter import ./numeric.bend as N import ./map_index.bend as Index import ./string_compare.bend as NatLaws
Definitions
def stride source · line 14 · raw
@+value:Nat -> {Nat.divmod(2n+value, 2n) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/proofs/map_index.next_quotient(Nat.divmod(value, 2n)) : Pair(Nat, Nat)}The binary constructor in the independent specification uses Base Nat.divmod. Establish its behavior against that existing algorithm, for arbitrary Nat.
def binary_division source · line 17 · raw
@value:Nat -> @+bit:Bool -> {Nat.divmod(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(value)), 2n) == (value, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit)) : Pair(Nat, Nat)}
def binary_quotient source · line 30 · raw
@+value:Nat -> @+bit:Bool -> {Nat.div(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(value)), 2n) == value : Nat}
def binary_remainder source · line 33 · raw
@+value:Nat -> @+bit:Bool -> {Nat.mod(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(value)), 2n) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit) : Nat}
def bit_roundtrip source · line 36 · raw
@bit:Bool -> {Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), 1n) == bit : Bool}
def binary_constructor source · line 41 · raw
@+n:Nat -> @+value:Nat -> @+bit:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(1n+n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(value))) == WCon{bit, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, value)} : Word(1n+n)}
def regroup source · line 48 · raw
@+bit:Bool -> @+value:Nat -> @+multiple:Nat -> {Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(value)), Nat.double(multiple)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bit), Nat.double(Nat.add(value, multiple))) : Nat}Reconstruct the low n bits after adding ANY multiple of 2^n. This is a universally quantified modular law, not bounded test enumeration.
def reconstruct source · line 51 · raw
@+n:Nat -> @word:Word(n) -> @+multiple:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.scale_binary(n, multiple))) == word : Word(n)}
def add_refines_n source · line 64 · raw
@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.adc(n, a, b, False{}, False{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, a), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, b))) : Word(n)}Actual full-width ripple addition equals independent mathematical conversion. ripple addition at any width: the checker never expands a literal-width word
def add_refines source · line 68 · raw
@+a:Word(64n) -> @+b:Word(64n) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.add(a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(64n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(64n, a), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(64n, b))) : Word(64n)}
def time_add_refines source · line 71 · raw
@a:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> @b:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/time.add(a, b) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.add(a, b) : 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64}
def increment_refines source · line 77 · raw
@+n:Nat -> @+word:Word(n) -> {Word.inc(n, word) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, 1n+0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word)) : Word(n)}The same reconstruction discharges wraparound for every metric counter.
def counter_refines source · line 81 · raw
@+word:Word(64n) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/src/wide.inc(word) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(64n, 1n+0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(64n, word)) : Word(64n)}