1	import Base
2	import ./row_major_index.bend as RowMajor
3	import ./natural_addition.bend as Addition
4	import ./word_arithmetic.bend as WordArithmetic
5	import ./nat_to_u32_bounds.bend as Bounds
6	
7	def truncate(n: Nat,w: Word(1n+n)) -> Word(n):
8	  match n:
9	    case 0n:
10	      WNil{}
11	    case 1n+p:
12	      WCon{b,t} = w
13	      WCon{b,truncate(p,t)}
14	
15	def truncate_zero(+n: Nat) -> {truncate(n,Word.zero(1n+n)) == Word.zero(n) : Word(n)}:
16	  match n:
17	    case 0n:
18	      {==}
19	    case 1n+ +p:
20	      %truncate_zero(p) : {WCon{False{},truncate(p,Word.zero(1n+p))} == WCon{False{},_} : Word(1n+p)}
21	      {==}
22	
23	def truncate_inc(+n: Nat,+w: Word(1n+n)) -> {truncate(n,Word.inc(1n+n,w)) == Word.inc(n,truncate(n,w)) : Word(n)}:
24	  match n:
25	    case 0n:
26	      {==}
27	    case 1n+ +p:
28	      match w:
29	        case WCon{False{},t}:
30	          {==}
31	        case WCon{True{},+t}:
32	          %truncate_inc(p,t) : {WCon{False{},truncate(p,Word.inc(1n+p,t))} == WCon{False{},_} : Word(1n+p)}
33	          {==}
34	
35	def truncate_encode(+a: Nat,+n: Nat) -> {truncate(n,WordArithmetic.encode(a,1n+n)) == WordArithmetic.encode(a,n) : Word(n)}:
36	  match a:
37	    case 0n:
38	      truncate_zero(n)
39	    case 1n+ +p:
40	      %Equal.sym(Word(n),truncate(n,Word.inc(1n+n,WordArithmetic.encode(p,1n+n))),Word.inc(n,truncate(n,WordArithmetic.encode(p,1n+n))),
41	        truncate_inc(n,WordArithmetic.encode(p,1n+n))) : {_ == Word.inc(n,WordArithmetic.encode(p,n)) : Word(n)}
42	      %truncate_encode(p,n) : {Word.inc(n,truncate(n,WordArithmetic.encode(p,1n+n))) == Word.inc(n,_) : Word(n)}
43	      {==}
44	
45	def put(+n: Nat,+b: Bool,+w: Word(n)) -> {Word.shl.put(n,b,w) == truncate(n,WCon{b,w}) : Word(n)}:
46	  match n:
47	    case 0n:
48	      {==}
49	    case 1n+ +p:
50	      WCon{+c,+t} = w
51	      %put(p,c,t) : {WCon{b,Word.shl.put(p,c,t)} == WCon{b,_} : Word(1n+p)}
52	      {==}
53	
54	def shift(+n: Nat,+w: Word(1n+n)) -> {Word.shl(1n+n,w) == WCon{False{},truncate(n,w)} : Word(1n+n)}:
55	  WCon{+b,+t} = w
56	  %put(n,b,t) : {WCon{False{},Word.shl.put(n,b,t)} == WCon{False{},_} : Word(1n+n)}
57	  {==}
58	
59	def encoded_double(+a: Nat,+n: Nat) -> {WordArithmetic.encode(Nat.double(a),1n+n) == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}:
60	  %Equal.sym(Word(1n+n),WordArithmetic.encode(Nat.double(a),1n+n),Word.shl(1n+n,WordArithmetic.encode(a,1n+n)),WordArithmetic.encode_double(a,
61	      1n+n)) : {_ == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}
62	  %Equal.sym(Word(1n+n),Word.shl(1n+n,WordArithmetic.encode(a,1n+n)),WCon{False{},truncate(n,WordArithmetic.encode(a,1n+n))},shift(n,
63	      WordArithmetic.encode(a,1n+n))) : {_ == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}
64	  %truncate_encode(a,n) : {WCon{False{},truncate(n,WordArithmetic.encode(a,1n+n))} == WCon{False{},_} : Word(1n+n)}
65	  {==}
66	
67	law word_roundtrip:
68	  for +n: Nat
69	  for +w: Word(n)
70	  {WordArithmetic.encode(Word.to_nat(n,w),n) == w : Word(n)}
71	def word_roundtrip(n,w):
72	  match n:
73	    case 0n:
74	      WNil{} = w
75	      {==}
76	    case 1n+ +p:
77	      match w:
78	        case WCon{False{},+t}:
79	          %Equal.sym(Word(1n+p),WordArithmetic.encode(Nat.double(Word.to_nat(p,t)),1n+p),WCon{False{},WordArithmetic.encode(Word.to_nat(p,t),p)},
80	            encoded_double(Word.to_nat(p,t),p)) : {_ == WCon{False{},t} : Word(1n+p)}
81	          %Equal.sym(Word(p),WordArithmetic.encode(Word.to_nat(p,t),p),t,word_roundtrip(p,t)) : {WCon{False{},_} == WCon{False{},t} : Word(1n+p)}
82	          {==}
83	        case WCon{True{},+t}:
84	          %Equal.sym(Word(1n+p),WordArithmetic.encode(Nat.double(Word.to_nat(p,t)),1n+p),WCon{False{},WordArithmetic.encode(Word.to_nat(p,t),p)},
85	            encoded_double(Word.to_nat(p,t),p)) : {Word.inc(1n+p,_) == WCon{True{},t} : Word(1n+p)}
86	          %Equal.sym(Word(p),WordArithmetic.encode(Word.to_nat(p,t),p),t,word_roundtrip(p,t)) : {WCon{True{},_} == WCon{True{},t} : Word(1n+p)}
87	          {==}
88	
89	def double_mul(+a: Nat,+b: Nat) -> {Nat.mul(Nat.double(a),b) == Nat.mul(a,Nat.double(b)) : Nat}:
90	  match a:
91	    case 0n:
92	      {==}
93	    case 1n+ +p:
94	      %Addition.double(b) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == Nat.add(_,Nat.mul(p,Nat.double(b))) : Nat}
95	      %Equal.sym(Nat,Nat.add(Nat.add(b,b),Nat.mul(p,Nat.double(b))),Nat.add(b,Nat.add(b,Nat.mul(p,Nat.double(b)))),Addition.associative(b,b,Nat.mul(p,
96	            Nat.double(b)))) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == _ : Nat}
97	      %double_mul(p,b) : {Nat.add(b,Nat.add(b,Nat.mul(Nat.double(p),b))) == Nat.add(b,Nat.add(b,_)) : Nat}
98	      {==}
99	
100	law multiply_go:
101	  for +m: Nat
102	  for +n: Nat
103	  for +w: Word(m)
104	  for +b: Nat
105	  for +acc: Nat
106	  {Word.mul.go(n,m,w,WordArithmetic.encode(b,n),WordArithmetic.encode(acc,n)) == WordArithmetic.encode(Nat.add(acc,Nat.mul(Word.to_nat(m,w),b)),
107	      n) : Word(n)}
108	def multiply_go(m,n,w,b,acc):
109	  match m:
110	    case 0n:
111	      %Equal.sym(Nat,Nat.add(acc,0n),acc,Addition.zero_right(acc)) : {WordArithmetic.encode(acc,n) == WordArithmetic.encode(_,n) : Word(n)}
112	      {==}
113	    case 1n+ +p:
114	      match w:
115	        case WCon{False{},+t}:
116	          %WordArithmetic.encode_double(b,n) : {Word.mul.go(n,p,t,_,WordArithmetic.encode(acc,n)) == WordArithmetic.encode(Nat.add(acc,
117	                Nat.mul(Nat.double(Word.to_nat(p,t)),b)),n) : Word(n)}
118	          %Equal.sym(Nat,Nat.mul(Nat.double(Word.to_nat(p,t)),b),Nat.mul(Word.to_nat(p,t),Nat.double(b)),double_mul(Word.to_nat(p,t),
119	              b)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),WordArithmetic.encode(acc,n)) == WordArithmetic.encode(Nat.add(acc,
120	                _),n) : Word(n)}
121	          multiply_go(p,n,t,Nat.double(b),acc)
122	        case WCon{True{},+t}:
123	          %WordArithmetic.encode_double(b,n) : {Word.mul.go(n,p,t,_,Word.add(n,WordArithmetic.encode(acc,n),WordArithmetic.encode(b,
124	                  n))) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,Nat.mul(Nat.double(Word.to_nat(p,t)),b))),n) : Word(n)}
125	          %Equal.sym(Word(n),Word.add(n,WordArithmetic.encode(acc,n),WordArithmetic.encode(b,n)),WordArithmetic.encode(Nat.add(acc,b),n),
126	            WordArithmetic.encode_add(acc,b,n)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),
127	              _) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,Nat.mul(Nat.double(Word.to_nat(p,t)),b))),n) : Word(n)}
128	          %Equal.sym(Nat,Nat.mul(Nat.double(Word.to_nat(p,t)),b),Nat.mul(Word.to_nat(p,t),Nat.double(b)),double_mul(Word.to_nat(p,t),
129	              b)) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),WordArithmetic.encode(Nat.add(acc,b),
130	                n)) == WordArithmetic.encode(Nat.add(acc,Nat.add(b,_)),n) : Word(n)}
131	          %Addition.associative(acc,b,Nat.mul(Word.to_nat(p,t),Nat.double(b))) : {Word.mul.go(n,p,t,WordArithmetic.encode(Nat.double(b),n),
132	              WordArithmetic.encode(Nat.add(acc,b),n)) == WordArithmetic.encode(_,n) : Word(n)}
133	          multiply_go(p,n,t,Nat.double(b),Nat.add(acc,b))
134	
135	def multiply(+n: Nat,+a: Word(n),+b: Word(n)) -> {Word.mul(n,a,b) == WordArithmetic.encode(Nat.mul(Word.to_nat(n,a),Word.to_nat(n,b)),n) : Word(n)}:
136	  %word_roundtrip(n,b) : {Word.mul.go(n,n,a,_,Word.zero(n)) == WordArithmetic.encode(Nat.mul(Word.to_nat(n,a),Word.to_nat(n,b)),n) : Word(n)}
137	  multiply_go(n,n,a,Word.to_nat(n,b),0n)
138	
139	def native_multiply(+a: U32,+b: U32) -> {U32.mul(a,b) == U32.from_nat(Nat.mul(U32.to_nat(a),U32.to_nat(b))) : U32}:
140	  match a b:
141	    case U32{+x} U32{+y}:
142	      %Equal.sym(U32,U32.from_nat(Nat.mul(Word.to_nat(32n,x),Word.to_nat(32n,y))),U32{WordArithmetic.encode(Nat.mul(Word.to_nat(32n,x),
143	              Word.to_nat(32n,y)),32n)},WordArithmetic.native_encoding(Nat.mul(Word.to_nat(32n,x),Word.to_nat(32n,y)))) : {U32{Word.mul(32n,x,
144	            y)} == _ : U32}
145	      %multiply(32n,x,y) : {U32{Word.mul(32n,x,y)} == U32{_} : U32}
146	      {==}
147	
148	def bounded_multiply(+a: U32,+b: U32,+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},h: {Nat.is_le(Nat.mul(U32.to_nat(a),
149	        U32.to_nat(b)),U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32.mul(a,b)) == Nat.mul(U32.to_nat(a),U32.to_nat(b)) : Nat}:
150	  %Equal.sym(U32,U32.mul(a,b),U32.from_nat(Nat.mul(U32.to_nat(a),U32.to_nat(b))),native_multiply(a,b)) : {U32.to_nat(_) == Nat.mul(U32.to_nat(a),
151	      U32.to_nat(b)) : Nat}
152	  Bounds.roundtrip(Nat.mul(U32.to_nat(a),U32.to_nat(b)),cap,cap_ok,h)
153	
154	# Encoding respects products even when the natural operands exceed a word.
155	def encoded_product_roundtrip(+value: Nat,remaining: Nat,+width: Nat) ->
156	  {WordArithmetic.encode(Nat.mul(Word.to_nat(width,WordArithmetic.encode(value,width)),remaining),width) == WordArithmetic.encode(Nat.mul(value,remaining),width) : Word(width)}:
157	  match remaining:
158	    case 0n:
159	      Equal.cong(Nat,Word(width),n => WordArithmetic.encode(n,width),Nat.mul(Word.to_nat(width,WordArithmetic.encode(value,width)),0n),Nat.mul(value,0n),
160	        Equal.trans(Nat,Nat.mul(Word.to_nat(width,WordArithmetic.encode(value,width)),0n),0n,Nat.mul(value,0n),RowMajor.multiply_zero_right(Word.to_nat(width,WordArithmetic.encode(value,width))),Equal.sym(Nat,Nat.mul(value,0n),0n,RowMajor.multiply_zero_right(value))))
161	    case 1n+ +rest:
162	      +decoded = Word.to_nat(width,WordArithmetic.encode(value,width))
163	      %Equal.sym(Nat,Nat.mul(decoded,1n+rest),Nat.add(decoded,Nat.mul(decoded,rest)),RowMajor.multiply_successor_right(decoded,rest)) :
164	        {WordArithmetic.encode(_,width) == WordArithmetic.encode(Nat.mul(value,1n+rest),width) : Word(width)}
165	      %Equal.sym(Nat,Nat.mul(value,1n+rest),Nat.add(value,Nat.mul(value,rest)),RowMajor.multiply_successor_right(value,rest)) :
166	        {WordArithmetic.encode(Nat.add(decoded,Nat.mul(decoded,rest)),width) == WordArithmetic.encode(_,width) : Word(width)}
167	      %WordArithmetic.encode_add(decoded,Nat.mul(decoded,rest),width) :
168	        {_ == WordArithmetic.encode(Nat.add(value,Nat.mul(value,rest)),width) : Word(width)}
169	      %WordArithmetic.encode_add(value,Nat.mul(value,rest),width) :
170	        {Word.add(width,WordArithmetic.encode(decoded,width),WordArithmetic.encode(Nat.mul(decoded,rest),width)) == _ : Word(width)}
171	      %Equal.sym(Word(width),WordArithmetic.encode(decoded,width),WordArithmetic.encode(value,width),word_roundtrip(width,WordArithmetic.encode(value,width))) :
172	        {Word.add(width,_,WordArithmetic.encode(Nat.mul(decoded,rest),width)) == Word.add(width,WordArithmetic.encode(value,width),WordArithmetic.encode(Nat.mul(value,rest),width)) : Word(width)}
173	      %Equal.sym(Word(width),WordArithmetic.encode(Nat.mul(decoded,rest),width),WordArithmetic.encode(Nat.mul(value,rest),width),encoded_product_roundtrip(value,rest,width)) :
174	        {Word.add(width,WordArithmetic.encode(value,width),_) == Word.add(width,WordArithmetic.encode(value,width),WordArithmetic.encode(Nat.mul(value,rest),width)) : Word(width)}
175	      {==}
176	
177	def encoded_multiply(+left: Nat,+right: Nat,+width: Nat) ->
178	  {Word.mul(width,WordArithmetic.encode(left,width),WordArithmetic.encode(right,width)) == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}:
179	  +a = Word.to_nat(width,WordArithmetic.encode(left,width))
180	  +b = Word.to_nat(width,WordArithmetic.encode(right,width))
181	  %Equal.sym(Word(width),Word.mul(width,WordArithmetic.encode(left,width),WordArithmetic.encode(right,width)),WordArithmetic.encode(Nat.mul(a,b),width),multiply(width,WordArithmetic.encode(left,width),WordArithmetic.encode(right,width))) :
182	    {_ == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}
183	  %Equal.sym(Word(width),WordArithmetic.encode(Nat.mul(a,b),width),WordArithmetic.encode(Nat.mul(left,b),width),encoded_product_roundtrip(left,b,width)) :
184	    {_ == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}
185	  %Equal.sym(Nat,Nat.mul(left,b),Nat.mul(b,left),RowMajor.multiply_commutative(left,b)) :
186	    {WordArithmetic.encode(_,width) == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}
187	  %Equal.sym(Word(width),WordArithmetic.encode(Nat.mul(b,left),width),WordArithmetic.encode(Nat.mul(right,left),width),encoded_product_roundtrip(right,left,width)) :
188	    {_ == WordArithmetic.encode(Nat.mul(left,right),width) : Word(width)}
189	  Equal.cong(Nat,Word(width),n => WordArithmetic.encode(n,width),Nat.mul(right,left),Nat.mul(left,right),RowMajor.multiply_commutative(right,left))
190	
191	def native_encoded_multiply(+left: Nat,+right: Nat) ->
192	  {(U32.from_nat(left) * U32.from_nat(right) : U32) == U32.from_nat(Nat.mul(left,right)) : U32}:
193	  %Equal.sym(U32,U32.from_nat(left),U32{WordArithmetic.encode(left,32n)},WordArithmetic.native_encoding(left)) :
194	    {(_ * U32.from_nat(right) : U32) == U32.from_nat(Nat.mul(left,right)) : U32}
195	  %Equal.sym(U32,U32.from_nat(right),U32{WordArithmetic.encode(right,32n)},WordArithmetic.native_encoding(right)) :
196	    {(U32{WordArithmetic.encode(left,32n)} * _ : U32) == U32.from_nat(Nat.mul(left,right)) : U32}
197	  %Equal.sym(U32,U32.from_nat(Nat.mul(left,right)),U32{WordArithmetic.encode(Nat.mul(left,right),32n)},WordArithmetic.native_encoding(Nat.mul(left,right))) :
198	    {U32{Word.mul(32n,WordArithmetic.encode(left,32n),WordArithmetic.encode(right,32n))} == _ : U32}
199	  Equal.cong(Word(32n),U32,word => U32{word},Word.mul(32n,WordArithmetic.encode(left,32n),WordArithmetic.encode(right,32n)),WordArithmetic.encode(Nat.mul(left,right),32n),encoded_multiply(left,right,32n))