~/bend-docscommunity

proofs/math/number/fixprime.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend as Fixprime

17 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/fixed.bend as SF
import ../../../spec/math/number.bend as SN
import ../../../src/math/fixed.bend as F
import ../../../src/math/number.bend as NB
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ./prime.bend as PR
import ../typed/width.bend as WW
import ../typed/w64add.bend as WA
import ../typed/w64mul.bend as W64M
import ../typed/u32laws.bend as LW
import ../u64/u64.bend as P64
import ../../lib/u32alg.bend as UA
import ../../lib/u32.bend as U3

Definitions

def v source · line 27 · raw

@+x:U32 -> Nat

def is_prime source · line 30 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.IsPrime.value(a)

def zc_t source · line 35 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:Nat -> @+x:Nat -> @+e:{Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == Nat.add(x, 1n) : Nat} -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.bn(Nat.is_eq(r, 0n)) == one : Nat}

def zc source · line 47 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:Nat -> @+x:Nat -> @+c:Bool -> @+e:{Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(c, one))) == Nat.add(x, 1n) : Nat} -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, x) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.bn(Nat.is_eq(r, 0n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(c, one) : Nat}

def bn_bo source · line 57 · raw

@+b:Bool -> @+c:Bool -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+e:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.bn(b) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(c, one) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(b, one) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(c, one) : Nat}

the position of m + 1 is 1 + the value of m

def succ_t source · line 68 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:U32 -> {Nat.add(v(U32.add(m, 1)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(U32.is_zero(U32.add(m, 1)), one))) == 1n+v(m) : Nat}

def at_val source · line 77 · raw

@+m:U32 -> @+t:Nat -> @+ht:{Nat.add(v(m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0n)) == t : Nat} -> {v(m) == t : Nat}

an unwrapped candidate sits at its value

def prime_of source · line 80 · raw

@+m:U32 -> @+pr:Bool -> @+hpr:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.is_prime(v(m)) == pr : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(v(m)) == pr : Bool}

def here source · line 85 · raw

@+n:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(n) == True{} : Bool} -> {Bool.and(Bool.and(Nat.is_le(n, n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(n)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.no_prime(Nat.sub(n, n), n)) == True{} : Bool}

def step_found source · line 91 · raw

@+t:Nat -> @+q:Nat -> @+pt:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(t) == False{} : Bool} -> @+ih:{Bool.and(Bool.and(Nat.is_le(1n+t, q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.no_prime(Nat.sub(q, 1n+t), 1n+t)) == True{} : Bool} -> {Bool.and(Bool.and(Nat.is_le(t, q), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.no_prime(Nat.sub(q, t), t)) == True{} : Bool}

def found_go source · line 102 · raw

@fuel:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:U32 -> @+wr:Bool -> @+hwr:{U32.is_zero(m) == wr : Bool} -> @+pr:Bool -> @+hpr:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.is_prime(v(m)) == pr : Bool} -> @+t:Nat -> @+ht:{Nat.add(v(m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(wr, one))) == t : Nat} -> @+p:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_np(fuel, m, wr, pr) == Some{p} : Maybe<&2, U32>} -> {Bool.and(Bool.and(Nat.is_le(t, v(p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(v(p))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.no_prime(Nat.sub(v(p), t), t)) == True{} : Bool}

def le_c source · line 122 · raw

@+a:Nat -> @+b:Nat -> @+d:Bool -> @+hd:{Nat.is_le(1n+a, b) == d : Bool} -> @+hc:{Nat.is_lt(a, b) == False{} : Bool} -> {False{} == d : Bool}

is_lt(a, b) is is_le(a + 1, b)

def lt_iff_c source · line 129 · raw

@+a:Nat -> @+b:Nat -> @+c:Bool -> @+hc:{Nat.is_lt(a, b) == c : Bool} -> {c == Nat.is_le(1n+a, b) : Bool}

def lt_iff source · line 136 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_lt(a, b) == Nat.is_le(1n+a, b) : Bool}

def found_one source · line 139 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> @+p:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_next_prime(n) == Some{p} : Maybe<&2, U32>} -> {Bool.and(Bool.and(Nat.is_le(1n+v(n), v(p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(v(p))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.no_prime(Nat.sub(v(p), 1n+v(n)), 1n+v(n))) == True{} : Bool}

def found source · line 143 · raw

@+n:U32 -> @+p:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_next_prime(n) == Some{p} : Maybe<&2, U32>} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.NextPrime.found(n, p, h)

def not_value_one source · line 151 · raw

@+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Word(n) -> {Nat.add(1n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32alg.uw(n, Word.not(n, b)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32alg.uw(n, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32alg.sc(n, one) : Nat}

UA.not_value with the unit kept open (n is 32 at the use)

def fuel_ok source · line 154 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), Nat.add(1n+v(n), 1n+v(U32.not(n)))) == True{} : Bool}

def fuel_ok2 source · line 171 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), Nat.add(1n+v(n), Nat.add(v(U32.not(n)), 1n))) == True{} : Bool}

2^32 stays C.shift(32, one) for a symbolic one: with one == 1n the checker would expand the closed 2^32 in unary

def beyond source · line 174 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+t:Nat -> @+q:Nat -> @+hS:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), t) == True{} : Bool} -> @+hq:{Nat.is_le(t, q) == True{} : Bool} -> @+hqf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, q) == True{} : Bool} -> Empty

def none_go source · line 177 · raw

@fuel:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:U32 -> @+wr:Bool -> @+hwr:{U32.is_zero(m) == wr : Bool} -> @+pr:Bool -> @+hpr:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.is_prime(v(m)) == pr : Bool} -> @+t:Nat -> @+ht:{Nat.add(v(m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(wr, one))) == t : Nat} -> @+hf:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one), Nat.add(t, fuel)) == True{} : Bool} -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_np(fuel, m, wr, pr) == None{} : Maybe<&2, U32>} -> @+q:Nat -> @+hq:{Nat.is_le(t, q) == True{} : Bool} -> @+hqf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, q) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(t, q) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(q) == False{} : Bool}

def none_one source · line 201 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_next_prime(n) == None{} : Maybe<&2, U32>} -> @+m:Nat -> @+hm:{Nat.is_lt(v(n), m) == True{} : Bool} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, m) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.prime(m) == False{} : Bool}

def none source · line 205 · raw

@+n:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_next_prime(n) == None{} : Maybe<&2, U32>} -> @+m:Nat -> @+hm:{Nat.is_lt(v(n), m) == True{} : Bool} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, m) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.NextPrime.none(n, h, m, hm, hf)