1	import Base
2	import ./logic.bend as L
3	import ./nat.bend as N
4	import ./u32.bend as U
5	import ../../spec/lib/common.bend as SC
6	import ./lemmas/spec/numeric.bend as S
7	
8	# U32 halving as a Nat operation, and the midpoint bounds.
9	#
10	# proofs/lib/u32.bend deliberately avoids `U32.add` (its comment explains
11	# why: `inc`/`shl`/`shr`/`sub` have Nat meanings that can be stated with a
12	# bound `i < 2^k` for a variable k). The graph's binary search needs the
13	# midpoint `(lo + hi) / 2`, so the two missing bridges are proved here from
14	# the retained word lemmas: full-width ripple addition conserves the value
15	# `shr` is exact halving, so the midpoint can be written with sub and shr
16	# alone.
17	
18	# ---- halving ----
19	
20	# The Nat halving the checker can compute structurally (no Nat.div).
21	def hlf(n: Nat) -> Nat:
22	  match n:
23	    case 0n:
24	      0n
25	    case 1n+p:
26	      match p:
27	        case 0n:
28	          0n
29	        case 1n+q:
30	          1n+hlf(q)
31	
32	def hlf_double(+q: Nat) -> {hlf(Nat.double(q)) == q : Nat}:
33	  match q:
34	    case 0n:
35	      {==}
36	    case 1n+p:
37	      Equal.cong(Nat, Nat, n => 1n+n, hlf(Nat.double(p)), p, hlf_double(p))
38	
39	def hlf_double_succ(+q: Nat) -> {hlf(1n+Nat.double(q)) == q : Nat}:
40	  match q:
41	    case 0n:
42	      {==}
43	    case 1n+p:
44	      Equal.cong(Nat, Nat, n => 1n+n, hlf(1n+Nat.double(p)), p, hlf_double_succ(p))
45	
46	def hlf_bit(+b: Bool, +q: Nat) -> {hlf(Nat.add(S.bit_value(b), Nat.double(q))) == q : Nat}:
47	  match b:
48	    case False{}:
49	      hlf_double(q)
50	    case True{}:
51	      hlf_double_succ(q)
52	
53	def shr_value(+x: U32) -> {U32.to_nat(U32.shr(x)) == hlf(U32.to_nat(x)) : Nat}:
54	  %Equal.sym(Nat, U32.to_nat(x), Nat.add(S.bit_value(U.low_bit(x)), Nat.double(U32.to_nat(U32.shr(x)))), U.shr_split(x)) : {U32.to_nat(U32.shr(x)) == hlf(_) : Nat}
55	  Equal.sym(Nat, hlf(Nat.add(S.bit_value(U.low_bit(x)), Nat.double(U32.to_nat(U32.shr(x))))), U32.to_nat(U32.shr(x)),
56	    hlf_bit(U.low_bit(x), U32.to_nat(U32.shr(x))))
57	
58	# ---- halving respects the order ----
59	
60	def hlf_le(+n: Nat) -> {Nat.is_le(hlf(n), n) == True{} : Bool}:
61	  match n:
62	    case 0n:
63	      {==}
64	    case 1n+p:
65	      match p:
66	        case 0n:
67	          {==}
68	        case 1n+q:
69	          N.le_trans(hlf(q), q, 1n+q, hlf_le(q), N.le_succ(q))
70	
71	def hlf_succ_le(+q: Nat) -> {Nat.is_le(hlf(1n+q), q) == True{} : Bool}:
72	  match q:
73	    case 0n:
74	      {==}
75	    case 1n+r:
76	      hlf_le(r)
77	
78	# The midpoint of a nonempty range lies inside it: a <= hlf(a+b) < b
79	# whenever a < b.
80	def hlf_lower(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(a, hlf(Nat.add(a, b))) == True{} : Bool}:
81	  match a b:
82	    case 0n b0:
83	      N.zero_le(hlf(Nat.add(0n, b0)))
84	    case 1n+p 0n:
85	      Empty.absurd({Nat.is_le(1n+p, hlf(Nat.add(1n+p, 0n))) == True{} : Bool}, L.false_true(h))
86	    case 1n+ +p 1n+ +q:
87	      %Equal.sym(Nat, Nat.add(p, 1n+q), 1n+Nat.add(p, q), N.add_succ(p, q)) : {Nat.is_le(1n+p, hlf(1n+_)) == True{} : Bool}
88	      hlf_lower(p, q, h)
89	
90	def hlf_upper(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(hlf(Nat.add(a, b)), b) == True{} : Bool}:
91	  match a b:
92	    case 0n 0n:
93	      Empty.absurd({Nat.is_lt(hlf(Nat.add(0n, 0n)), 0n) == True{} : Bool}, L.false_true(h))
94	    case 0n 1n+ +q:
95	      N.le_lt_trans(hlf(1n+q), q, 1n+q, hlf_succ_le(q), N.lt_succ(q))
96	    case 1n+p 0n:
97	      Empty.absurd({Nat.is_lt(hlf(Nat.add(1n+p, 0n)), 0n) == True{} : Bool}, L.false_true(h))
98	    case 1n+ +p 1n+ +q:
99	      %Equal.sym(Nat, Nat.add(p, 1n+q), 1n+Nat.add(p, q), N.add_succ(p, q)) : {Nat.is_lt(hlf(1n+_), 1n+q) == True{} : Bool}
100	      hlf_upper(p, q, h)
101	
102	# ---- from_nat / sub bridges used with the halving one ----
103	
104	# The graph implementation avoids `U32.add` entirely (its Nat meaning would
105	# need a 2^32 bound, and the checker cannot expand 2^32 as a unary Nat), so
106	# only halving and subtraction bridges are needed. Subtraction is
107	# proofs/lib/u32.bend `sub_nat`; halving is `shr_value` above.
108	
109	def hlf_bound(+i: Nat, +k: Nat, +h: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {Nat.is_lt(hlf(i), SC.pow2(k)) == True{} : Bool}:
110	  N.le_lt_trans(hlf(i), i, SC.pow2(k), hlf_le(i), h)
111	
112	def shr_bridge(+i: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {U32.shr(U32.from_nat(i)) == U32.from_nat(hlf(i)) : U32}:
113	  +ri = U.to_nat_from_nat(i, k, hk, hi)
114	  U.injective(U32.shr(U32.from_nat(i)), U32.from_nat(hlf(i)),
115	    Equal.trans(Nat, U32.to_nat(U32.shr(U32.from_nat(i))), hlf(i), U32.to_nat(U32.from_nat(hlf(i))),
116	      Equal.trans(Nat, U32.to_nat(U32.shr(U32.from_nat(i))), hlf(U32.to_nat(U32.from_nat(i))), hlf(i),
117	        shr_value(U32.from_nat(i)),
118	        Equal.cong(Nat, Nat, hlf, U32.to_nat(U32.from_nat(i)), i, ri)),
119	      Equal.sym(Nat, U32.to_nat(U32.from_nat(hlf(i))), hlf(i),
120	        U.to_nat_from_nat(hlf(i), k, hk, hlf_bound(i, k, hi)))))
121	
122	# ---- the halving measure used by the binary search ----
123	
124	# s < 2m gives s/2 < m: one narrowing step of a search range that started
125	# below 2^f lands below 2^(f-1).
126	def hlf_lt(+s: Nat, +m: Nat, +h: {Nat.is_lt(s, Nat.double(m)) == True{} : Bool}) -> {Nat.is_lt(hlf(s), m) == True{} : Bool}:
127	  match s m:
128	    case s0 0n:
129	      Empty.absurd({Nat.is_lt(hlf(s0), 0n) == True{} : Bool}, N.lt_zero_absurd(s0, h))
130	    case 0n 1n+q:
131	      {==}
132	    case 1n+0n 1n+q:
133	      {==}
134	    case 1n+1n+r 1n+q:
135	      hlf_lt(r, q, h)
136	
137	# The size after one step is at most s/2, so it stays below the halved bound.
138	def step_bound(+s2: Nat, +s: Nat, +m: Nat, +hle: {Nat.is_le(s2, hlf(s)) == True{} : Bool}, +h: {Nat.is_lt(s, Nat.double(m)) == True{} : Bool}) -> {Nat.is_lt(s2, m) == True{} : Bool}:
139	  N.le_lt_trans(s2, hlf(s), m, hle, hlf_lt(s, m, h))
140	
141	# ---- subtraction bridge ----
142	
143	# U32.sub is exact whenever the subtrahend is not larger (no borrow), so it
144	# is the Nat subtraction of the two indices.
145	def sub_le(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
146	  match a b:
147	    case a0 0n:
148	      L.subst(Nat, z => {Nat.is_le(z, a0) == True{} : Bool}, a0, Nat.sub(a0, 0n), Equal.sym(Nat, Nat.sub(a0, 0n), a0, N.sub_zero(a0)), N.le_refl(a0))
149	    case 0n 1n+q:
150	      N.zero_le(Nat.sub(0n, 1n+q))
151	    case 1n+p 1n+q:
152	      N.le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), N.le_succ(p))
153	
154	def sub_bridge(+a: Nat, +b: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +ha: {Nat.is_lt(a, SC.pow2(k)) == True{} : Bool}, +hb: {Nat.is_le(b, a) == True{} : Bool}) -> {U32.sub(U32.from_nat(a), U32.from_nat(b)) == U32.from_nat(Nat.sub(a, b)) : U32}:
155	  +hb2 = N.le_lt_trans(b, a, SC.pow2(k), hb, ha)
156	  +ra = U.to_nat_from_nat(a, k, hk, ha)
157	  +rb = U.to_nat_from_nat(b, k, hk, hb2)
158	  +le = L.subst(Nat, z => {Nat.is_le(z, U32.to_nat(U32.from_nat(a))) == True{} : Bool}, b, U32.to_nat(U32.from_nat(b)), Equal.sym(Nat, U32.to_nat(U32.from_nat(b)), b, rb),
159	          L.subst(Nat, z => {Nat.is_le(b, z) == True{} : Bool}, a, U32.to_nat(U32.from_nat(a)), Equal.sym(Nat, U32.to_nat(U32.from_nat(a)), a, ra), hb))
160	  U.injective(U32.sub(U32.from_nat(a), U32.from_nat(b)), U32.from_nat(Nat.sub(a, b)),
161	    Equal.trans(Nat, U32.to_nat(U32.sub(U32.from_nat(a), U32.from_nat(b))), Nat.sub(a, b), U32.to_nat(U32.from_nat(Nat.sub(a, b))),
162	      Equal.trans(Nat, U32.to_nat(U32.sub(U32.from_nat(a), U32.from_nat(b))), Nat.sub(U32.to_nat(U32.from_nat(a)), U32.to_nat(U32.from_nat(b))), Nat.sub(a, b),
163	        U.sub_nat(U32.from_nat(a), U32.from_nat(b), le),
164	        Equal.trans(Nat, Nat.sub(U32.to_nat(U32.from_nat(a)), U32.to_nat(U32.from_nat(b))), Nat.sub(a, U32.to_nat(U32.from_nat(b))), Nat.sub(a, b),
165	          Equal.cong(Nat, Nat, z => Nat.sub(z, U32.to_nat(U32.from_nat(b))), U32.to_nat(U32.from_nat(a)), a, ra),
166	          Equal.cong(Nat, Nat, z => Nat.sub(a, z), U32.to_nat(U32.from_nat(b)), b, rb))),
167	      Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.sub(a, b))), Nat.sub(a, b),
168	        U.to_nat_from_nat(Nat.sub(a, b), k, hk, N.le_lt_trans(Nat.sub(a, b), a, SC.pow2(k), sub_le(a, b), ha)))))