spec/math/instances.bend

bend-collections-laws-crypto@1.0.0.0 · 89 lines · 17 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/src/math/num.bend as N
4import bend-collections-laws-crypto@1.0.0.0/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
39def Ops.zero(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat) -> Type:
40  {val(op(N.ZeroOp{})) == 0n : Nat}
41
42def Ops.one(~T: Data, ~op: N.Op<T> -> T, ~val: T -> Nat) -> Type:
43  {val(op(N.One{})) == 1n : Nat}
44
45def 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
48def 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
51def 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
54def 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
57def 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
60def 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
63def 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
66def 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
69def 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
72def 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
75def 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
79def Ops.abs(~T: Data, ~op: N.Op<T> -> T, +a: T) -> Type:
80  {op(N.Abs{a}) == a : T}
81
82def 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
85def 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
88def 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}