proofs/math/typed/u32.bend

bend-collections-laws-math@1.0.0.0 · 179 lines · 23 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
3import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
5import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
6import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
7import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
8import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
10import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
11import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
12import bend-collections-laws-math@1.0.0.0/proofs/lib/words32.bend as W32
13import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
14
15# The cheap clauses of spec/math/generic.bend proved at U32 for every input:
16# Abs.identity, Min.agrees, Max.agrees, Sign.agrees and Clamp.agrees (the selections go
17# through U32.is_lt, which is Nat's order on the values). The other U32
18# clauses and every U64, F32 and F64 clause are stated and tested
19# (docs/MATH_CONTRACTS.md).
20
21# ---- Nat.min and Nat.max from the order ----
22
23def min_of_ge(+a: Nat, +b: Nat, +h: {Nat.is_lt(b, a) == False{} : Bool}) -> {Nat.min(a, b) == a : Nat}:
24  match a b:
25    case 0n bb:
26      {==}
27    case 1n+ap 0n:
28      Empty.absurd({Nat.min(1n+ap, 0n) == 1n+ap : Nat}, N.zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h))))
29    case 1n+ap 1n+bp:
30      N.succ_cong(Nat.min(ap, bp), ap, min_of_ge(ap, bp, h))
31
32def min_of_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(b, a) == True{} : Bool}) -> {Nat.min(a, b) == b : Nat}:
33  match a b:
34    case 0n bb:
35      Empty.absurd({Nat.min(0n, bb) == bb : Nat}, N.lt_zero_absurd(bb, h))
36    case 1n+ap 0n:
37      {==}
38    case 1n+ap 1n+bp:
39      N.succ_cong(Nat.min(ap, bp), bp, min_of_lt(ap, bp, h))
40
41def max_of_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.max(a, b) == b : Nat}:
42  match a b:
43    case 0n bb:
44      {==}
45    case 1n+ap 0n:
46      Empty.absurd({Nat.max(1n+ap, 0n) == 0n : Nat}, N.lt_zero_absurd(1n+ap, h))
47    case 1n+ap 1n+bp:
48      N.succ_cong(Nat.max(ap, bp), bp, max_of_lt(ap, bp, h))
49
50def max_of_ge(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.max(a, b) == a : Nat}:
51  match a b:
52    case 0n 0n:
53      {==}
54    case 0n 1n+bp:
55      Empty.absurd({Nat.max(0n, 1n+bp) == 0n : Nat}, N.zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h))))
56    case 1n+ap 0n:
57      {==}
58    case 1n+ap 1n+bp:
59      N.succ_cong(Nat.max(ap, bp), ap, max_of_ge(ap, bp, h))
60
61# ---- U32 round trip ----
62
63# (one and k stay symbolic, so 2^32 is never expanded)
64def val_lt(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {k == 32n : Nat}, +a: U32) -> {Nat.is_lt(U32.to_nat(a), SC.pow2(k)) == True{} : Bool}:
65  %Equal.sym(Nat, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k)) : {Nat.is_lt(U32.to_nat(a), _) == True{} : Bool}
66  %Equal.sym(Nat, k, 32n, hk) : {Nat.is_lt(U32.to_nat(a), WD.sc(_, one)) == True{} : Bool}
67  UD.vb(one, h1, a)
68
69def le_k(+k: Nat, +hk: {k == 32n : Nat}) -> {Nat.is_le(k, 32n) == True{} : Bool}:
70  %Equal.sym(Nat, k, 32n, hk) : {Nat.is_le(_, 32n) == True{} : Bool}
71  {==}
72
73# a U32 is the U32 of its value
74def round_trip_k(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {k == 32n : Nat}, +a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
75  U.injective(U32.from_nat(U32.to_nat(a)), a, U.to_nat_from_nat(U32.to_nat(a), k, le_k(k, hk), val_lt(one, h1, k, hk, a)))
76
77def round_trip(+a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
78  round_trip_k(1n, {==}, 32n, {==}, a)
79
80# ---- the clauses ----
81
82def abs_identity(+x: U32) -> SG.Abs.identity(~U32, ~I.u32_op, ~I.u32_is, x):
83  {==}
84
85def min_c(+a: U32, +b: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(b), U32.to_nat(a)) == c : Bool}) -> {G.pick(U32, c, b, a) == U32.from_nat(Nat.min(U32.to_nat(a), U32.to_nat(b))) : U32}:
86  match c:
87    case True{}:
88      %Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b), min_of_lt(U32.to_nat(a), U32.to_nat(b), hc)) : {b == U32.from_nat(_) : U32}
89      Equal.sym(U32, U32.from_nat(U32.to_nat(b)), b, round_trip(b))
90    case False{}:
91      %Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a), min_of_ge(U32.to_nat(a), U32.to_nat(b), hc)) : {a == U32.from_nat(_) : U32}
92      Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, round_trip(a))
93
94def min_agrees(+a: U32, +b: U32) -> SG.Min.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b):
95  %Equal.sym(Bool, U32.is_lt(b, a), Nat.is_lt(U32.to_nat(b), U32.to_nat(a)), U.is_lt_nat(b, a)) : {G.pick(U32, _, b, a) == U32.from_nat(Nat.min(U32.to_nat(a), U32.to_nat(b))) : U32}
96  min_c(a, b, Nat.is_lt(U32.to_nat(b), U32.to_nat(a)), {==})
97
98def max_c(+a: U32, +b: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == c : Bool}) -> {G.pick(U32, c, b, a) == U32.from_nat(Nat.max(U32.to_nat(a), U32.to_nat(b))) : U32}:
99  match c:
100    case True{}:
101      %Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b), max_of_lt(U32.to_nat(a), U32.to_nat(b), hc)) : {b == U32.from_nat(_) : U32}
102      Equal.sym(U32, U32.from_nat(U32.to_nat(b)), b, round_trip(b))
103    case False{}:
104      %Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a), max_of_ge(U32.to_nat(a), U32.to_nat(b), hc)) : {a == U32.from_nat(_) : U32}
105      Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, round_trip(a))
106
107def max_agrees(+a: U32, +b: U32) -> SG.Max.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b):
108  %Equal.sym(Bool, U32.is_lt(a, b), Nat.is_lt(U32.to_nat(a), U32.to_nat(b)), U.is_lt_nat(a, b)) : {G.pick(U32, _, b, a) == U32.from_nat(Nat.max(U32.to_nat(a), U32.to_nat(b))) : U32}
109  max_c(a, b, Nat.is_lt(U32.to_nat(a), U32.to_nat(b)), {==})
110
111# ---- sign: 1 above zero, else the value itself (0) ----
112
113def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
114  N.zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h)))
115
116def lt_zero_false(+n: Nat) -> {Nat.is_lt(n, 0n) == False{} : Bool}:
117  match n:
118    case 0n:
119      {==}
120    case 1n+p:
121      {==}
122
123# 0 < n gives not n < 1
124def pos_ge_one(+n: Nat, +h: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(n, 1n) == False{} : Bool}:
125  match n:
126    case 0n:
127      Empty.absurd({Nat.is_lt(0n, 1n) == False{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
128    case 1n+p:
129      lt_zero_false(p)
130
131# not 0 < n gives n < 1
132def zero_lt_one(+n: Nat, +h: {Nat.is_lt(0n, n) == False{} : Bool}) -> {Nat.is_lt(n, 1n) == True{} : Bool}:
133  match n:
134    case 0n:
135      {==}
136    case 1n+p:
137      Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, true_ne_false(h))
138
139def sign_c(+x: U32, +c: Bool, +hc: {Nat.is_lt(0n, U32.to_nat(x)) == c : Bool}) -> {G.sign_above(~U32, ~I.u32_op, ~I.u32_is, x, c) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}:
140  match c:
141    case True{}:
142      %Equal.sym(Nat, Nat.min(U32.to_nat(x), 1n), 1n, N.min_right(U32.to_nat(x), 1n, pos_ge_one(U32.to_nat(x), hc))) : {1 == U32.from_nat(_) : U32}
143      {==}
144    case False{}:
145      %Equal.sym(Bool, U32.is_lt(x, 0), Nat.is_lt(U32.to_nat(x), 0n), U.is_lt_nat(x, 0)) : {G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, _) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}
146      %Equal.sym(Bool, Nat.is_lt(U32.to_nat(x), 0n), False{}, lt_zero_false(U32.to_nat(x))) : {G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, _) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}
147      %Equal.sym(Nat, Nat.min(U32.to_nat(x), 1n), U32.to_nat(x), N.min_left(U32.to_nat(x), 1n, zero_lt_one(U32.to_nat(x), hc))) : {x == U32.from_nat(_) : U32}
148      Equal.sym(U32, U32.from_nat(U32.to_nat(x)), x, round_trip(x))
149
150def sign_agrees(+x: U32) -> SG.Sign.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, x):
151  %Equal.sym(Bool, U32.is_lt(0, x), Nat.is_lt(0n, U32.to_nat(x)), U.is_lt_nat(0, x)) : {G.sign_above(~U32, ~I.u32_op, ~I.u32_is, x, _) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}
152  sign_c(x, Nat.is_lt(0n, U32.to_nat(x)), {==})
153
154# ---- clamp: Domain when hi < lo, else min(max(x, lo), hi) ----
155
156def max_val_c(+x: U32, +lo: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)) == c : Bool}) -> {U32.to_nat(G.pick(U32, c, lo, x)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}:
157  match c:
158    case True{}:
159      Equal.sym(Nat, Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(lo), max_of_lt(U32.to_nat(x), U32.to_nat(lo), hc))
160    case False{}:
161      Equal.sym(Nat, Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(x), max_of_ge(U32.to_nat(x), U32.to_nat(lo), hc))
162
163# the value of max(x, lo) is the larger value
164def max_val(+x: U32, +lo: U32) -> {U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}:
165  %Equal.sym(Bool, U32.is_lt(x, lo), Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)), U.is_lt_nat(x, lo)) : {U32.to_nat(G.pick(U32, _, lo, x)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}
166  max_val_c(x, lo, Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)), {==})
167
168def clamp_c(+x: U32, +lo: U32, +hi: U32, +c: Bool) -> {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp_ok(U32.to_nat(x), U32.to_nat(lo), U32.to_nat(hi), c)) : Result<&2, &2, NM.NumError, U32>}:
169  match c:
170    case True{}:
171      {==}
172    case False{}:
173      %Equal.sym(U32, G.min(~U32, ~I.u32_op, ~I.u32_is, G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo), hi), U32.from_nat(Nat.min(U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)), U32.to_nat(hi))), min_agrees(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo), hi)) : {Done{_} == Done{U32.from_nat(Nat.min(Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(hi)))} : Result<&2, &2, NM.NumError, U32>}
174      %Equal.sym(Nat, U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)), Nat.max(U32.to_nat(x), U32.to_nat(lo)), max_val(x, lo)) : {Done{U32.from_nat(Nat.min(_, U32.to_nat(hi)))} == Done{U32.from_nat(Nat.min(Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(hi)))} : Result<&2, &2, NM.NumError, U32>}
175      {==}
176
177def clamp_agrees(+x: U32, +lo: U32, +hi: U32) -> SG.Clamp.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, x, lo, hi):
178  %Equal.sym(Bool, U32.is_lt(hi, lo), Nat.is_lt(U32.to_nat(hi), U32.to_nat(lo)), U.is_lt_nat(hi, lo)) : {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, _) == SG.lift(~U32, ~SG.u32_of, M.clamp(U32.to_nat(x), U32.to_nat(lo), U32.to_nat(hi))) : Result<&2, &2, NM.NumError, U32>}
179  clamp_c(x, lo, hi, Nat.is_lt(U32.to_nat(hi), U32.to_nat(lo)))