1	import Base
2	import ../../src/math/u64.bend as U
3	import ../../src/math/hash.bend as HS
4	import ../../src/math/pow2.bend as PW
5	import ../lib/lemmas/spec/numeric.bend as S
6	import ../lib/lemmas/types/model.bend as T
7	import ../../spec/lib/common.bend as SC
8	import ./pow2/pow2.bend as P2
9	import ./u64/u64.bend as P
10	import ./u64/u64div.bend as PD
11	import ../lib/u32div.bend as UD
12	import ./hash/hash.bend as PH
13	import ../lib/word.bend as WD
14	import ../lib/lemmas/proofs/word_addition.bend as WA
15	import ./natural/proof.bend as NT
16	import ../../spec/math/u64.bend as SU
17	import ../../spec/math/hash.bend as SH
18	import ../../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
27	def 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	
30	def 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
34	def u64_is_zero(+a: U.U64) -> SU.IsZero.value(a):
35	  P.is_zero(a)
36	
37	def u64_le_signed(+a: U.U64, +b: U.U64) -> SU.LeSigned.value(a, b):
38	  P.le_signed(a, b)
39	
40	def u64_add(+a: U.U64, +b: U.U64) -> SU.Add.bits(a, b):
41	  P.add(a, b)
42	
43	def 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	
46	def u64_neg(+a: U.U64) -> SU.Neg.bits(a):
47	  P.neg(a)
48	
49	def 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	
52	def 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	
55	def 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
59	def hash_bucket_le(+w: U32, +mask: U32) -> SH.Bucket.le(w, mask):
60	  PH.bucket_le(w, mask)
61	
62	def 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
66	def pow2(+d: Nat) -> SP.Pow2t.value(d):
67	  P2.same(d)