proofs/math/proof.bend
bend-collections-laws-containers@1.0.0.0 · 67 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as U
3import bend-collections-laws-containers@1.0.0.0/src/math/hash.bend as HS
4import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as PW
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-containers@1.0.0.0/proofs/math/pow2/pow2.bend as P2
9import bend-collections-laws-containers@1.0.0.0/proofs/math/u64/u64.bend as P
10import bend-collections-laws-containers@1.0.0.0/proofs/math/u64/u64div.bend as PD
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
12import bend-collections-laws-containers@1.0.0.0/proofs/math/hash/hash.bend as PH
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/word.bend as WD
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as WA
15import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/proof.bend as NT
16import bend-collections-laws-containers@1.0.0.0/spec/math/u64.bend as SU
17import bend-collections-laws-containers@1.0.0.0/spec/math/hash.bend as SH
18import bend-collections-laws-containers@1.0.0.0/spec/math/pow2.bend as SP
19
20# Gate for src/math: every contract clause of spec/math/{pow2,hash,u64}.bend,
21# under the clause's name (natural.bend's clauses are proved in
22# natural/proof.bend), plus Base's U32 division against Nat and the cache
23# model's milliseconds. The word model is spec/lib/numeric.bend; none
24# assumes a hole or an axiom.
25
26# U32 long division (Base's U32.div / U32.mod), every nonzero divisor
27def u32_div(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {U32.to_nat(U32.div(a, b)) == Nat.div(U32.to_nat(a), U32.to_nat(b)) : Nat}:
28 UD.div_nat(a, b, hb)
29
30def u32_mod(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {U32.to_nat(U32.mod(a, b)) == Nat.mod(U32.to_nat(a), U32.to_nat(b)) : Nat}:
31 UD.mod_nat(a, b, hb)
32
33# u64
34def u64_is_zero(+a: U.U64) -> SU.IsZero.value(a):
35 P.is_zero(a)
36
37def u64_le_signed(+a: U.U64, +b: U.U64) -> SU.LeSigned.value(a, b):
38 P.le_signed(a, b)
39
40def u64_add(+a: U.U64, +b: U.U64) -> SU.Add.bits(a, b):
41 P.add(a, b)
42
43def u64_add_modular(+a: U.U64, +b: U.U64) -> SU.Add.modular(a, b):
44 Equal.trans(Word(64n), P.bits(U.add(a, b)), Word.add(64n, P.bits(a), P.bits(b)), S.from_nat(64n, Nat.add(S.unsigned(64n, P.bits(a)), S.unsigned(64n, P.bits(b)))), P.add(a, b), WA.refines(64n, P.bits(a), P.bits(b)))
45
46def u64_neg(+a: U.U64) -> SU.Neg.bits(a):
47 P.neg(a)
48
49def u64_div_small(+a: U.U64, +d: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, 1048576) == True{} : Bool}) -> SU.DivSmall.quotient(a, d, hd0, hle):
50 PD.div_bits(a, d, hd0, hle)
51
52def u64_div_small_signed(+a: U.U64, +d: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, 1048576) == True{} : Bool}) -> SU.DivSmallSigned.quotient(a, d, hd0, hle):
53 PD.div_signed(a, d, hd0, hle)
54
55def u64_milliseconds(+a: U.U64) -> {T.I64{P.bits(U.div_small_signed(a, 1000000))} == S.milliseconds(T.I64{P.bits(a)}) : T.Int64}:
56 PD.milliseconds(a)
57
58# hash
59def hash_bucket_le(+w: U32, +mask: U32) -> SH.Bucket.le(w, mask):
60 PH.bucket_le(w, mask)
61
62def hash_bucket_lt(+w: U32, +k: Nat, +mask: U32, +hm: {mask == U32{WD.mask(32n, k)} : U32}) -> SH.Bucket.lt(w, k, mask, hm):
63 PH.bucket_lt(w, k, mask, hm)
64
65# pow2
66def pow2(+d: Nat) -> SP.Pow2t.value(d):
67 P2.same(d)