1	import Base
2	
3	# The 64-bit word model: a Word(n) denotes the natural number of its bits
4	# (least significant first), and machine operations are specified through
5	# Nat arithmetic (modulo 2^n, unsigned and signed quotients). Shared by the
6	# src/math specs (u64, w64, hash) and by the proofs about words and U32s.
7	
8	# Independent mathematical interpretation. Nat here is a specification value;
9	# no public executable conversion of a 64-bit number through Nat is required.
10	def bit_value(b: Bool) -> Nat:
11	  match b:
12	    case False{}:
13	      0n
14	    case True{}:
15	      1n
16	
17	def unsigned(n: Nat, w: Word(n)) -> Nat:
18	  match n:
19	    case 0n:
20	      0n
21	    case 1n+p:
22	      match w:
23	        case WCon{b, tail}:
24	          Nat.add(bit_value(b), Nat.double(unsigned(p, tail)))
25	
26	def sign_threshold(n: Nat) -> Word(1n+n):
27	  match n:
28	    case 0n:
29	      WCon{True{}, WNil{}}
30	    case 1n+p:
31	      WCon{False{}, sign_threshold(p)}
32	
33	def negative(+w: Word(64n)) -> Bool:
34	  Cmp.is_ge(Word.cmp(64n, w, sign_threshold(63n)))
35	
36	def zero(w: Word(64n)) -> Bool:
37	  Cmp.is_eq(Word.cmp(64n, w, Word.zero(64n)))
38	
39	def order(a: Word(64n), b: Word(64n), sign_a: Bool, sign_b: Bool) -> Bool:
40	  match sign_a sign_b:
41	    case False{} True{}:
42	      False{}
43	    case True{} False{}:
44	      True{}
45	    case x y:
46	      Cmp.is_le(Word.cmp(64n, a, b))
47	
48	# These mathematical definitions specify modulo arithmetic through Nat values,
49	# independently of the implementation's ripple addition and binary long division.
50	def from_nat(n: Nat, +value: Nat) -> Word(n):
51	  match n:
52	    case 0n:
53	      WNil{}
54	    case 1n+p:
55	      WCon{Nat.is_eq(Nat.mod(value, 2n), 1n), from_nat(p, Nat.div(value, 2n))}
56	
57	def modulus() -> Nat:
58	  Nat.pow(2n, 64n)
59	
60	# Observe the input constructor before evaluating mathematical division. This
61	# has the same from_nat(unsigned(input) / divisor) meaning; the structural guard
62	# keeps fixed large denominators from being expanded while input is unknown.
63	def unsigned_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
64	  match n:
65	    case 0n: WNil{}
66	    case 1n+ +p:
67	      match word:
68	        case WCon{bit, tail}:
69	          from_nat(1n+p, Nat.div(unsigned(1n+p, WCon{bit, tail}), U32.to_nat(d)))
70	
71	def negative_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
72	  match n:
73	    case 0n: WNil{}
74	    case 1n+ +p:
75	      match word:
76	        case WCon{bit, tail}:
77	          from_nat(1n+p, Nat.sub(Nat.pow(2n, 1n+p), Nat.div(Nat.sub(Nat.pow(2n, 1n+p), unsigned(1n+p, WCon{bit, tail})), U32.to_nat(d))))
78	
79	def quotient_signed(bits: Word(64n), negative: Bool) -> Word(64n):
80	  match negative:
81	    case False{}:
82	      unsigned_quotient(64n, bits, 1000000)
83	    case True{}:
84	      negative_quotient(64n, bits, 1000000)
85	
86	# Mathematical multiplication by 2^places, specified without machine shifts.
87	def scale_binary(places: Nat, value: Nat) -> Nat:
88	  match places:
89	    case 0n:
90	      value
91	    case 1n+p:
92	      Nat.double(scale_binary(p, value))
93	
94	# A 64-bit word from two 32-bit limbs (low first).
95	def join(n: Nat, +m: Nat, a: Word(n), b: Word(m)) -> Word(Nat.add(n, m)):
96	  match n:
97	    case 0n:
98	      b
99	    case 1n+p:
100	      match a:
101	        case WCon{h, tail}:
102	          WCon{h, join(p, m, tail, b)}
103	
104	def pack(low: U32, high: U32) -> Word(64n):
105	  match low high:
106	    case U32{lo} U32{hi}:
107	      join(32n, 32n, lo, hi)
108	
109	# The low k bits set, the rest clear.
110	def mask(+n: Nat, +k: Nat) -> Word(n):
111	  match n k:
112	    case 0n _:
113	      WNil{}
114	    case 1n+p 0n:
115	      WCon{False{}, mask(p, 0n)}
116	    case 1n+p 1n+j:
117	      WCon{True{}, mask(p, j)}