1	import Base
2	import ../lib/common.bend as C
3	import ../../src/math/num.bend as N
4	import ../../src/math/natural.bend as M
5	
6	# Specification of src/math/num.bend's interface and of the instances in
7	# src/math/instances.bend (and f64.bend's): what each Op and Test must
8	# compute for the generic functions (spec/math/generic.bend) to meet their
9	# contracts. num.bend itself is the interface's types; its laws are these.
10	#
11	# Integer instances (U32 with width 32, U64 with width 64; val as in
12	# spec/math/generic.bend): every operation is the Nat operation on the
13	# values, formed only where it fits (generic.bend asks AddOver or MulOver
14	# first, and forms Sub, Quot, Rem, MulMod under their preconditions).
15	#
16	# Float instances (F32: Base's F32 primitives, F64: src/math/f64.bend's,
17	# specified by spec/math/f64.bend): Add, Sub, Mul, Quot, Neg, Abs are the
18	# IEEE operations of the type, Lt the IEEE order (false on NaN), and the
19	# over-tests are False (floats round instead of overflowing).
20	#
21	# STATED, TESTED, NOT PROVED: exercised through every generic function by
22	# tools/check_generic.py and at U32 by the checker-evaluated examples of
23	# proofs/math/typed/examples.bend.
24	#
25	#   Op / Test    clauses
26	#   Zero, One    Ops.zero, Ops.one
27	#   Add          Ops.add, Tests.add_over
28	#   Sub          Ops.sub
29	#   Mul          Ops.mul, Tests.mul_over
30	#   Quot, Rem    Ops.quot, Ops.rem
31	#   Half         Ops.half
32	#   MulMod       Ops.mulmod
33	#   Pow2         Ops.pow2
34	#   Sqrt         Ops.sqrt
35	#   Abs          Ops.abs
36	#   Lt, Odd,     Tests.lt, Tests.odd, Tests.is_zero
37	#   IsZero
38	
39	def Ops.zero(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat) -> Type:
40	  {val(op(N.ZeroOp{})) == 0n : Nat}
41	
42	def Ops.one(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat) -> Type:
43	  {val(op(N.One{})) == 1n : Nat}
44	
45	def Ops.add(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +a: T, +b: T, +h: {test(N.AddOver{a, b}) == False{} : Bool}) -> Type:
46	  {val(op(N.Add{a, b})) == Nat.add(val(a), val(b)) : Nat}
47	
48	def Tests.add_over(~T: Data, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +w: Nat, +a: T, +b: T) -> Type:
49	  {test(N.AddOver{a, b}) == Bool.not(C.fits(w, Nat.add(val(a), val(b)))) : Bool}
50	
51	def Ops.sub(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat, +a: T, +b: T, +h: {Nat.is_le(val(b), val(a)) == True{} : Bool}) -> Type:
52	  {val(op(N.Sub{a, b})) == Nat.sub(val(a), val(b)) : Nat}
53	
54	def Ops.mul(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +a: T, +b: T, +h: {test(N.MulOver{a, b}) == False{} : Bool}) -> Type:
55	  {val(op(N.Mul{a, b})) == Nat.mul(val(a), val(b)) : Nat}
56	
57	def Tests.mul_over(~T: Data, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +w: Nat, +a: T, +b: T) -> Type:
58	  {test(N.MulOver{a, b}) == Bool.not(C.fits(w, Nat.mul(val(a), val(b)))) : Bool}
59	
60	def Ops.quot(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat, +a: T, +b: T, +h: {Nat.is_eq(val(b), 0n) == False{} : Bool}) -> Type:
61	  {val(op(N.Quot{a, b})) == Nat.div(val(a), val(b)) : Nat}
62	
63	def Ops.rem(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat, +a: T, +b: T, +h: {Nat.is_eq(val(b), 0n) == False{} : Bool}) -> Type:
64	  {val(op(N.Rem{a, b})) == Nat.mod(val(a), val(b)) : Nat}
65	
66	def Ops.half(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat, +a: T) -> Type:
67	  {val(op(N.Half{a})) == Nat.div(val(a), 2n) : Nat}
68	
69	def Ops.mulmod(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat, +a: T, +b: T, +m: T, +ha: {Nat.is_lt(val(a), val(m)) == True{} : Bool}, +hb: {Nat.is_lt(val(b), val(m)) == True{} : Bool}) -> Type:
70	  {val(op(N.MulMod{a, b, m})) == Nat.mod(Nat.mul(val(a), val(b)), val(m)) : Nat}
71	
72	def Ops.pow2(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat, +w: Nat, +k: Nat, +hk: {Nat.is_lt(k, w) == True{} : Bool}) -> Type:
73	  {val(op(N.Pow2{k})) == C.pow2(k) : Nat}
74	
75	def Ops.sqrt(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat, +a: T) -> Type:
76	  {val(op(N.Sqrt{a})) == M.isqrt(val(a)) : Nat}
77	
78	# unsigned: |a| is a
79	def Ops.abs(~T: Data, ~op: N.Op<T> -> T, +a: T) -> Type:
80	  {op(N.Abs{a}) == a : T}
81	
82	def Tests.lt(~T: Data, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +a: T, +b: T) -> Type:
83	  {test(N.Lt{a, b}) == Nat.is_lt(val(a), val(b)) : Bool}
84	
85	def Tests.odd(~T: Data, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +a: T) -> Type:
86	  {test(N.Odd{a}) == Nat.is_eq(Nat.mod(val(a), 2n), 1n) : Bool}
87	
88	def Tests.is_zero(~T: Data, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +a: T) -> Type:
89	  {test(N.IsZero{a}) == Nat.is_eq(val(a), 0n) : Bool}