1	import Base
2	import ../lib/common.bend as C
3	import ../../src/math/u64.bend as W
4	import ../../src/math/w64.bend as X
5	import ../../src/math/natural.bend as M
6	
7	# Specification of src/math/w64.bend: unsigned 64-bit arithmetic on the
8	# two-limb U64 (low limb first). value(a) is the natural number a denotes;
9	# every operation is the Nat operation modulo 2^64 (C.low(64n, _): the
10	# checker never forms 2^64; spec/lib/common.bend), as in
11	# spec/math/u64.bend's word model (the two agree: value(a) is
12	# unsigned(64, bits(a))).
13	#
14	# STATED, TESTED, NOT PROVED: w64.bend is the U64 instance's engine; its
15	# clauses are exercised through tools/check_generic.py (every generic
16	# function at U64 against Python integers) and tools/check_f64.py (the
17	# software binary64's significand arithmetic), not proved.
18	#
19	#   function          clauses
20	#   mul32             Mul32.value
21	#   add, add_over     Add.value, AddOver.value
22	#   sub               Sub.value
23	#   mul, mul_over     Mul.value, MulOver.value
24	#   half, odd         Half.value, Odd.value
25	#   lt, le, eq,       Lt.value, Le.value, Eq.value, IsZero.value
26	#   is_zero
27	#   div32, mod32      Div32.quot, Div32.rem, Mod32.value
28	#   quot, rem         DivMod.quot, DivMod.rem
29	#   mulmod            MulMod.value
30	#   isqrt, isqrt32    Isqrt.value, Isqrt32.value
31	#   shl, shr,         Shl.value, Shr.value, ShrJam.value
32	#   shr_jam
33	#   clz               Clz.value
34	
35	def value(a: W.U64) -> Nat:
36	  match a:
37	    case W.U64{lo, hi}:
38	      Nat.add(U32.to_nat(lo), C.shift(32n, U32.to_nat(hi)))
39	
40	# the U64 of a value below 2^64
41	def of_nat(+n: Nat) -> W.U64:
42	  W.U64{U32.from_nat(C.low(32n, n)), U32.from_nat(C.high(32n, n))}
43	
44	def Mul32.value(+a: U32, +b: U32) -> Type:
45	  {value(X.mul32(a, b)) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
46	
47	def Add.value(+a: W.U64, +b: W.U64) -> Type:
48	  {value(X.add(a, b)) == C.low(64n, Nat.add(value(a), value(b))) : Nat}
49	
50	def AddOver.value(+a: W.U64, +b: W.U64) -> Type:
51	  {X.add_over(a, b) == Bool.not(C.fits(64n, Nat.add(value(a), value(b)))) : Bool}
52	
53	def Sub.value(+a: W.U64, +b: W.U64, +h: {Nat.is_le(value(b), value(a)) == True{} : Bool}) -> Type:
54	  {value(X.sub(a, b)) == Nat.sub(value(a), value(b)) : Nat}
55	
56	def Mul.value(+a: W.U64, +b: W.U64) -> Type:
57	  {value(X.mul(a, b)) == C.low(64n, Nat.mul(value(a), value(b))) : Nat}
58	
59	def MulOver.value(+a: W.U64, +b: W.U64) -> Type:
60	  {X.mul_over(a, b) == Bool.not(C.fits(64n, Nat.mul(value(a), value(b)))) : Bool}
61	
62	def Half.value(+a: W.U64) -> Type:
63	  {value(X.half(a)) == Nat.div(value(a), 2n) : Nat}
64	
65	def Odd.value(+a: W.U64) -> Type:
66	  {X.odd(a) == Nat.is_eq(Nat.mod(value(a), 2n), 1n) : Bool}
67	
68	def Lt.value(+a: W.U64, +b: W.U64) -> Type:
69	  {X.lt(a, b) == Nat.is_lt(value(a), value(b)) : Bool}
70	
71	def Le.value(+a: W.U64, +b: W.U64) -> Type:
72	  {X.le(a, b) == Nat.is_le(value(a), value(b)) : Bool}
73	
74	def Eq.value(+a: W.U64, +b: W.U64) -> Type:
75	  {X.eq(a, b) == Nat.is_eq(value(a), value(b)) : Bool}
76	
77	def IsZero.value(+a: W.U64) -> Type:
78	  {X.is_zero(a) == Nat.is_eq(value(a), 0n) : Bool}
79	
80	def Div32.quot(+a: W.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> Type:
81	  {value(X.fst_q(X.div32(a, d))) == Nat.div(value(a), U32.to_nat(d)) : Nat}
82	
83	def Div32.rem(+a: W.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> Type:
84	  {U32.to_nat(X.snd_r(X.div32(a, d))) == Nat.mod(value(a), U32.to_nat(d)) : Nat}
85	
86	def Mod32.value(+a: W.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> Type:
87	  {U32.to_nat(X.mod32(a, d)) == Nat.mod(value(a), U32.to_nat(d)) : Nat}
88	
89	def DivMod.quot(+a: W.U64, +b: W.U64, +hb: {X.is_zero(b) == False{} : Bool}) -> Type:
90	  {value(X.quot(a, b)) == Nat.div(value(a), value(b)) : Nat}
91	
92	def DivMod.rem(+a: W.U64, +b: W.U64, +hb: {X.is_zero(b) == False{} : Bool}) -> Type:
93	  {value(X.rem(a, b)) == Nat.mod(value(a), value(b)) : Nat}
94	
95	# a, b < m: the product reduced, with no 64-bit overflow on the way
96	def MulMod.value(+a: W.U64, +b: W.U64, +m: W.U64, +ha: {Nat.is_lt(value(a), value(m)) == True{} : Bool}, +hb: {Nat.is_lt(value(b), value(m)) == True{} : Bool}) -> Type:
97	  {value(X.mulmod(a, b, m)) == Nat.mod(Nat.mul(value(a), value(b)), value(m)) : Nat}
98	
99	# the integer square root of the proved Nat reference
100	def Isqrt.value(+n: W.U64) -> Type:
101	  {value(X.isqrt(n)) == M.isqrt(value(n)) : Nat}
102	
103	def Isqrt32.value(+x: U32) -> Type:
104	  {U32.to_nat(X.isqrt32(x)) == M.isqrt(U32.to_nat(x)) : Nat}
105	
106	def Shl.value(+a: W.U64, +k: Nat, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> Type:
107	  {value(X.shl(a, k)) == C.low(64n, C.shift(k, value(a))) : Nat}
108	
109	def Shr.value(+a: W.U64, +k: Nat) -> Type:
110	  {value(X.shr(a, k)) == C.high(k, value(a)) : Nat}
111	
112	# shifted right, with the shifted-out bits OR-ed into bit 0 (SoftFloat's
113	# softfloat_shiftRightJam64); jam(q, r) sets q's bit 0 when r is nonzero
114	def jam(+q: Nat, +r: Nat) -> Nat:
115	  Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(Nat.mod(q, 2n), Nat.min(r, 1n)))
116	
117	def ShrJam.value(+a: W.U64, +k: Nat) -> Type:
118	  {value(X.shr_jam(a, k)) == jam(C.high(k, value(a)), C.low(k, value(a))) : Nat}
119	
120	# 64 for zero
121	def Clz.value(+a: W.U64) -> Type:
122	  {X.clz(a) == Nat.sub(64n, M.bit_length(value(a))) : Nat}