1	# General-width bit-vector arithmetic used by the native-address obligation.
2	import Base
3	
4	def concat(+n: Nat, +m: Nat, w: Word(n), tail: Word(m)) -> Word(Nat.add(n,m)):
5	  match n:
6	    case 0n:
7	      match w:
8	        case WNil{}:
9	          tail
10	    case 1n+p:
11	      match w:
12	        case WCon{b,rest}:
13	          WCon{b,concat(p,m,rest,tail)}
14	
15	def shift(n: Nat, x: Nat) -> Nat:
16	  match n:
17	    case 0n:
18	      x
19	    case 1n+p:
20	      Nat.double(shift(p,x))
21	
22	law double_add:
23	  for +a: Nat
24	  for +b: Nat
25	  {Nat.double(Nat.add(a,b)) == Nat.add(Nat.double(a),Nat.double(b)) : Nat}
26	
27	def double_add(a,b):
28	  match a:
29	    case 0n:
30	      {==}
31	    case 1n+ +p:
32	      %double_add(p,b) : {2n+Nat.double(Nat.add(p,b)) == 2n+_ : Nat}
33	      {==}
34	
35	law zero_nat:
36	  for +n: Nat
37	  {Word.to_nat(n,Word.zero(n)) == 0n : Nat}
38	
39	def zero_nat(n):
40	  match n:
41	    case 0n:
42	      {==}
43	    case 1n+ +p:
44	      %zero_nat(p) : {Nat.double(Word.to_nat(p,Word.zero(p))) == Nat.double(_) : Nat}
45	      {==}
46	
47	law finish_lt_zero:
48	  for +b: Bool
49	  for +c: Cmp
50	  {Cmp.is_lt(Word.cmp.fin(b,False{},c)) == Cmp.is_lt(c) : Bool}
51	
52	def finish_lt_zero(b,c):
53	  match b c:
54	    case False{} LT{}:
55	      {==}
56	    case False{} EQ{}:
57	      {==}
58	    case False{} GT{}:
59	      {==}
60	    case True{} LT{}:
61	      {==}
62	    case True{} EQ{}:
63	      {==}
64	    case True{} GT{}:
65	      {==}
66	
67	law compare_high_only:
68	  for +n: Nat
69	  for +m: Nat
70	  for +w: Word(n)
71	  for +top: Word(m)
72	  for +other: Word(m)
73	  {Cmp.is_lt(Word.cmp(Nat.add(n,m),concat(n,m,w,top),concat(n,m,Word.zero(n),other))) == Cmp.is_lt(Word.cmp(m,top,other)) : Bool}
74	
75	def compare_high_only(n,m,w,top,other):
76	  match n:
77	    case 0n:
78	      match w:
79	        case WNil{}:
80	          {==}
81	    case 1n+ +p:
82	      match w:
83	        case WCon{+b,+rest}:
84	          %compare_high_only(p,m,rest,top,other) : {Cmp.is_lt(Word.cmp.fin(b,False{},Word.cmp(Nat.add(p,m),concat(p,m,rest,top),concat(p,m,
85	                  Word.zero(p),other)))) == _ : Bool}
86	          finish_lt_zero(b,Word.cmp(Nat.add(p,m),concat(p,m,rest,top),concat(p,m,Word.zero(p),other)))
87	
88	law nonnegative:
89	  for +n: Nat
90	  for +w: Word(n)
91	  {Cmp.is_lt(Word.cmp(n,w,Word.zero(n))) == False{} : Bool}
92	
93	def nonnegative(n,w):
94	  match n:
95	    case 0n:
96	      match w:
97	        case WNil{}:
98	          {==}
99	    case 1n+ +p:
100	      match w:
101	        case WCon{+b,+rest}:
102	          %nonnegative(p,rest) : {Cmp.is_lt(Word.cmp.fin(b,False{},Word.cmp(p,rest,Word.zero(p)))) == _ : Bool}
103	          finish_lt_zero(b,Word.cmp(p,rest,Word.zero(p)))
104	
105	def truth(b: Bool) -> Type:
106	  match b:
107	    case False{}:
108	      Empty
109	    case True{}:
110	      Unit
111	
112	def false_true(e: {False{} == True{} : Bool}) -> Empty:
113	  %Equal.sym(Bool,False{},True{},e) : truth(_)
114	  Unit{}
115	
116	law finish_one:
117	  for +b: Bool
118	  for +c: Cmp
119	  for nonneg: {Cmp.is_lt(c) == False{} : Bool}
120	  {Cmp.is_lt(Word.cmp.fin(b,True{},c)) == Cmp.is_eq(Word.cmp.fin(b,False{},c)) : Bool}
121	
122	def finish_one(b,c,nonneg):
123	  match b c:
124	    case False{} LT{}:
125	      Empty.absurd({True{} == False{} : Bool},false_true(Equal.sym(Bool,True{},False{},nonneg)))
126	    case False{} EQ{}:
127	      {==}
128	    case False{} GT{}:
129	      {==}
130	    case True{} LT{}:
131	      Empty.absurd({True{} == False{} : Bool},false_true(Equal.sym(Bool,True{},False{},nonneg)))
132	    case True{} EQ{}:
133	      {==}
134	    case True{} GT{}:
135	      {==}
136	
137	law less_one_is_zero:
138	  for +n: Nat
139	  for +w: Word(1n+n)
140	  {Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})) == Cmp.is_eq(Word.cmp(1n+n,w,Word.zero(1n+n))) : Bool}
141	
142	def less_one_is_zero(n,w):
143	  match w:
144	    case WCon{b,+rest}:
145	      finish_one(b,Word.cmp(n,rest,Word.zero(n)),nonnegative(n,rest))
146	
147	type Split<-n: Nat,-m: Nat> is Data:
148	  Parts{low: Word(n),high: Word(m)}
149	
150	def join(+n: Nat, +m: Nat, parts: Split<n,m>) -> Word(Nat.add(n,m)):
151	  Parts{low,high} = parts
152	  concat(n,m,low,high)
153	
154	def prepend(-n: Nat, -m: Nat, b: Bool, parts: Split<n,m>) -> Split<1n+n,m>:
155	  Parts{low,high} = parts
156	  Parts{WCon{b,low},high}
157	
158	def split(+n: Nat, +m: Nat, w: Word(Nat.add(n,m))) -> Split<n,m>:
159	  match n:
160	    case 0n:
161	      Parts{WNil{},w}
162	    case 1n+ +p:
163	      match w:
164	        case WCon{b,rest}:
165	          prepend(p,m,b,split(p,m,rest))
166	
167	law join_prepend:
168	  for +n: Nat
169	  for +m: Nat
170	  for +b: Bool
171	  for +parts: Split<n,m>
172	  {WCon{b,join(n,m,parts)} == join(1n+n,m,prepend(n,m,b,parts)) : Word(1n+Nat.add(n,m))}
173	
174	def join_prepend(n,m,b,parts):
175	  Parts{low,high} = parts
176	  {==}
177	
178	law recover:
179	  for +n: Nat
180	  for +m: Nat
181	  for +w: Word(Nat.add(n,m))
182	  {join(n,m,split(n,m,w)) == w : Word(Nat.add(n,m))}
183	
184	def recover(n,m,w):
185	  match n:
186	    case 0n:
187	      {==}
188	    case 1n+ +p:
189	      match w:
190	        case WCon{+b,+rest}:
191	          %recover(p,m,rest) : {join(1n+p,m,prepend(p,m,b,split(p,m,rest))) == WCon{b,_} : Word(1n+Nat.add(p,m))}
192	          Equal.sym(Word(1n+Nat.add(p,m)),WCon{b,join(p,m,split(p,m,rest))},join(1n+p,m,prepend(p,m,b,split(p,m,rest))),join_prepend(p,m,b,
193	              split(p,m,rest)))
194	
195	law cmp_eq:
196	  for +c: Cmp
197	  for yes: {Cmp.is_eq(c) == True{} : Bool}
198	  {c == EQ{} : Cmp}
199	
200	def cmp_eq(c,yes):
201	  match c:
202	    case LT{}:
203	      Empty.absurd({LT{} == EQ{} : Cmp},false_true(yes))
204	    case EQ{}:
205	      {==}
206	    case GT{}:
207	      Empty.absurd({GT{} == EQ{} : Cmp},false_true(yes))
208	
209	law finish_eq_parts:
210	  for +b: Bool
211	  for +c: Cmp
212	  for eq: {Word.cmp.fin(b,False{},c) == EQ{} : Cmp}
213	  {b == False{} : Bool} & {c == EQ{} : Cmp}
214	
215	def finish_eq_parts(b,c,eq):
216	  match b c:
217	    case False{} LT{}:
218	      Empty.absurd({False{} == False{} : Bool} & {LT{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),LT{},EQ{},eq)))
219	    case False{} EQ{}:
220	      ({==},{==})
221	    case False{} GT{}:
222	      Empty.absurd({False{} == False{} : Bool} & {GT{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),GT{},EQ{},eq)))
223	    case True{} LT{}:
224	      Empty.absurd({True{} == False{} : Bool} & {LT{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),LT{},EQ{},eq)))
225	    case True{} EQ{}:
226	      Empty.absurd({True{} == False{} : Bool} & {EQ{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),GT{},EQ{},eq)))
227	    case True{} GT{}:
228	      Empty.absurd({True{} == False{} : Bool} & {GT{} == EQ{} : Cmp},false_true(Equal.cong(Cmp,Bool,c => Cmp.is_eq(c),GT{},EQ{},eq)))
229	
230	law zero_reflect:
231	  for +n: Nat
232	  for +w: Word(n)
233	  for eq: {Word.cmp(n,w,Word.zero(n)) == EQ{} : Cmp}
234	  {w == Word.zero(n) : Word(n)}
235	
236	def zero_step(+p: Nat, +b: Bool, +rest: Word(p), proof: {b == False{} : Bool} & {Word.cmp(p,rest,Word.zero(p)) == EQ{} : Cmp}, ih: {Word.cmp(p,
237	      rest,Word.zero(p)) == EQ{} : Cmp} -> {rest == Word.zero(p) : Word(p)}) -> {WCon{b,rest} == Word.zero(1n+p) : Word(1n+p)}:
238	  (head,tail) = proof
239	  %Equal.sym(Bool,b,False{},head) : {WCon{_,rest} == Word.zero(1n+p) : Word(1n+p)}
240	  %ih(tail) : {WCon{False{},rest} == WCon{False{},_} : Word(1n+p)}
241	  {==}
242	
243	def zero_reflect(n,w,eq):
244	  match n:
245	    case 0n:
246	      match w:
247	        case WNil{}:
248	          {==}
249	    case 1n+ +p:
250	      match w:
251	        case WCon{+b,+rest}:
252	          zero_step(p,b,rest,finish_eq_parts(b,Word.cmp(p,rest,Word.zero(p)),eq),e => zero_reflect(p,rest,e))
253	
254	law below_one_zero:
255	  for +n: Nat
256	  for +w: Word(1n+n)
257	  for below: {Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})) == True{} : Bool}
258	  {w == Word.zero(1n+n) : Word(1n+n)}
259	
260	def below_one_zero(n,w,below):
261	  zero_reflect(1n+n,w,cmp_eq(Word.cmp(1n+n,w,Word.zero(1n+n)),Equal.trans(Bool,Cmp.is_eq(Word.cmp(1n+n,w,Word.zero(1n+n))),
262	        Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})),True{},Equal.sym(Bool,Cmp.is_lt(Word.cmp(1n+n,w,WCon{True{},Word.zero(n)})),
263	          Cmp.is_eq(Word.cmp(1n+n,w,Word.zero(1n+n))),less_one_is_zero(n,w)),below)))
264	
265	law and_zero:
266	  for +n: Nat
267	  for +w: Word(n)
268	  {Word.and(n,w,Word.zero(n)) == Word.zero(n) : Word(n)}
269	
270	def and_zero(n,w):
271	  match n:
272	    case 0n:
273	      match w:
274	        case WNil{}:
275	          {==}
276	    case 1n+ +p:
277	      match w:
278	        case WCon{False{},+rest}:
279	          %and_zero(p,rest) : {WCon{False{},Word.and(p,rest,Word.zero(p))} == WCon{False{},_} : Word(1n+p)}
280	          {==}
281	        case WCon{True{},+rest}:
282	          %and_zero(p,rest) : {WCon{False{},Word.and(p,rest,Word.zero(p))} == WCon{False{},_} : Word(1n+p)}
283	          {==}
284	
285	law upper_zero:
286	  for +n: Nat
287	  for +m: Nat
288	  for +low: Word(n)
289	  for +high: Word(1n+m)
290	  for bound: {Cmp.is_lt(Word.cmp(Nat.add(n,1n+m),concat(n,1n+m,low,high),concat(n,1n+m,Word.zero(n),WCon{True{},Word.zero(m)}))) == True{} : Bool}
291	  {high == Word.zero(1n+m) : Word(1n+m)}
292	
293	def upper_zero(n,m,low,high,bound):
294	  below_one_zero(m,high,Equal.trans(Bool,Cmp.is_lt(Word.cmp(1n+m,high,WCon{True{},Word.zero(m)})),Cmp.is_lt(Word.cmp(Nat.add(n,1n+m),concat(n,
295	          1n+m,low,high),concat(n,1n+m,Word.zero(n),WCon{True{},Word.zero(m)}))),True{},Equal.sym(Bool,Cmp.is_lt(Word.cmp(Nat.add(n,1n+m),
296	          concat(n,1n+m,low,high),concat(n,1n+m,Word.zero(n),WCon{True{},Word.zero(m)}))),Cmp.is_lt(Word.cmp(1n+m,high,WCon{True{},
297	          Word.zero(m)})),compare_high_only(n,1n+m,low,high,WCon{True{},Word.zero(m)})),bound))