1	import Base
2	import ../lib/numeric.bend as N
3	import ../../src/math/u64.bend as U
4	
5	# Specification of src/math/u64.bend: a U64 denotes the 64-bit word whose
6	# low 32 bits are lo and high 32 bits hi (bits below), and each operation is
7	# the word operation of spec/lib/numeric.bend: modular addition, two's
8	# complement negation, signed order, unsigned and signed quotients by small
9	# divisors.
10	#
11	#   function          clauses                                   proved in
12	#   is_zero           IsZero.value                              proofs/math/proof.bend
13	#   le_signed         LeSigned.value                            (u64_*, via u64/u64.bend
14	#   add               Add.bits, Add.modular                      and u64/u64div.bend)
15	#   neg               Neg.bits
16	#   div_small         DivSmall.quotient
17	#   div_small_signed  DivSmallSigned.quotient
18	
19	def bits(a: U.U64) -> Word(64n):
20	  match a:
21	    case U.U64{lo, hi}:
22	      N.pack(lo, hi)
23	
24	# the quotient of a signed word: rounded toward zero, as the magnitude's
25	def signed_quotient(w: Word(64n), neg: Bool, +d: U32) -> Word(64n):
26	  match neg:
27	    case False{}:
28	      N.unsigned_quotient(64n, w, d)
29	    case True{}:
30	      N.negative_quotient(64n, w, d)
31	
32	def IsZero.value(+a: U.U64) -> Type:
33	  {U.is_zero(a) == N.zero(bits(a)) : Bool}
34	
35	def LeSigned.value(+a: U.U64, +b: U.U64) -> Type:
36	  {U.le_signed(a, b) == N.order(bits(a), bits(b), N.negative(bits(a)), N.negative(bits(b))) : Bool}
37	
38	def Add.bits(+a: U.U64, +b: U.U64) -> Type:
39	  {bits(U.add(a, b)) == Word.add(64n, bits(a), bits(b)) : Word(64n)}
40	
41	# addition modulo 2^64
42	def Add.modular(+a: U.U64, +b: U.U64) -> Type:
43	  {bits(U.add(a, b)) == N.from_nat(64n, Nat.add(N.unsigned(64n, bits(a)), N.unsigned(64n, bits(b)))) : Word(64n)}
44	
45	def Neg.bits(+a: U.U64) -> Type:
46	  {bits(U.neg(a)) == Word.inc(64n, Word.not(64n, bits(a))) : Word(64n)}
47	
48	# divisors 1 .. 2^20 (the limb division stays inside 32 bits)
49	def DivSmall.quotient(+a: U.U64, +d: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, 1048576) == True{} : Bool}) -> Type:
50	  {bits(U.div_small(a, d)) == N.unsigned_quotient(64n, bits(a), d) : Word(64n)}
51	
52	def DivSmallSigned.quotient(+a: U.U64, +d: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, 1048576) == True{} : Bool}) -> Type:
53	  {bits(U.div_small_signed(a, d)) == signed_quotient(bits(a), N.negative(bits(a)), d) : Word(64n)}