1	import Base
2	import ./natural_addition.bend as Addition
3	import ./word_encoding.bend as WordEncoding
4	import ./word_width.bend as WordWidth
5	
6	law pad_nat:
7	  for +n: Nat
8	  for +w: Word(n)
9	  {Word.to_nat(1n+n,Word.shr.pad(n,w)) == Word.to_nat(n,w) : Nat}
10	def pad_nat(n,w):
11	  match n:
12	    case 0n:
13	      match w:
14	        case WNil{}: {==}
15	    case 1n+ +p:
16	      match w:
17	        case WCon{False{},+t}:
18	          %pad_nat(p,t) : {Nat.double(Word.to_nat(1n+p,Word.shr.pad(p,t))) == Nat.double(_) : Nat}
19	          {==}
20	        case WCon{True{},+t}:
21	          %pad_nat(p,t) : {1n+Nat.double(Word.to_nat(1n+p,Word.shr.pad(p,t))) == 1n+Nat.double(_) : Nat}
22	          {==}
23	
24	law inc_nat:
25	  for +n: Nat
26	  for +w: Word(n)
27	  {Word.to_nat(1n+n,Word.inc(1n+n,Word.shr.pad(n,w))) == 1n+Word.to_nat(n,w) : Nat}
28	def inc_nat(n,w):
29	  match n:
30	    case 0n:
31	      match w:
32	        case WNil{}: {==}
33	    case 1n+ +p:
34	      match w:
35	        case WCon{False{},+t}:
36	          %pad_nat(p,t) : {1n+Nat.double(Word.to_nat(1n+p,Word.shr.pad(p,t))) == 1n+Nat.double(_) : Nat}
37	          {==}
38	        case WCon{True{},+t}:
39	          %inc_nat(p,t) : {Nat.double(Word.to_nat(1n+p,Word.inc(1n+p,Word.shr.pad(p,t)))) == Nat.double(_) : Nat}
40	          {==}
41	
42	law adc_zero:
43	  for +n: Nat
44	  for +w: Word(n)
45	  {Word.adc(n,w,Word.zero(n),False{},False{}) == w : Word(n)}
46	def adc_zero(n,w):
47	  match n:
48	    case 0n:
49	      WNil{} = w
50	      {==}
51	    case 1n+ +p:
52	      match w:
53	        case WCon{False{},+t}:
54	          %adc_zero(p,t) : {WCon{False{},Word.adc(p,t,Word.zero(p),False{},False{})} == WCon{False{},_} : Word(1n+p)}
55	          {==}
56	        case WCon{True{},+t}:
57	          %adc_zero(p,t) : {WCon{True{},Word.adc(p,t,Word.zero(p),False{},False{})} == WCon{True{},_} : Word(1n+p)}
58	          {==}
59	
60	law adc_one:
61	  for +n: Nat
62	  for +w: Word(n)
63	  {Word.adc(n,w,Word.zero(n),False{},True{}) == Word.inc(n,w) : Word(n)}
64	def adc_one(n,w):
65	  match n:
66	    case 0n:
67	      WNil{} = w
68	      {==}
69	    case 1n+ +p:
70	      match w:
71	        case WCon{False{},+t}:
72	          %adc_zero(p,t) : {WCon{True{},Word.adc(p,t,Word.zero(p),False{},False{})} == WCon{True{},_} : Word(1n+p)}
73	          {==}
74	        case WCon{True{},+t}:
75	          %adc_one(p,t) : {WCon{False{},Word.adc(p,t,Word.zero(p),False{},True{})} == WCon{False{},_} : Word(1n+p)}
76	          {==}
77	
78	law add_one:
79	  for +n: Nat
80	  for +w: Word(n)
81	  {Word.add(n,w,Word.inc(n,Word.zero(n))) == Word.inc(n,w) : Word(n)}
82	def add_one(n,w):
83	  match n:
84	    case 0n:
85	      {==}
86	    case 1n+ +p:
87	      match w:
88	        case WCon{False{},+t}:
89	          %adc_zero(p,t) : {WCon{True{},Word.adc(p,t,Word.zero(p),False{},False{})} == WCon{True{},_} : Word(1n+p)}
90	          {==}
91	        case WCon{True{},+t}:
92	          %adc_one(p,t) : {WCon{False{},Word.adc(p,t,Word.zero(p),False{},True{})} == WCon{False{},_} : Word(1n+p)}
93	          {==}
94	
95	law concat_pad:
96	  for +width: Nat
97	  for +word: Word(width)
98	  {WordWidth.transport(Nat.add(width,1n),1n+width,WordEncoding.concat(width,1n,word,Word.zero(1n)),
99	      Addition.successor_width(width)) == Word.shr.pad(width,word) : Word(1n+width)}
100	
101	def concat_pad(width,word):
102	  match width:
103	    case 0n:
104	      match word:
105	        case WNil{}:
106	          {==}
107	    case 1n+ +rest:
108	      match word:
109	        case WCon{+bit,+tail}:
110	          Equal.trans(Word(2n+rest),
111	            WordWidth.transport(1n+Nat.add(rest,1n),2n+rest,WCon{bit,WordEncoding.concat(rest,1n,tail,Word.zero(1n))},
112	              Addition.successor_width(1n+rest)),
113	            WCon{bit,WordWidth.transport(Nat.add(rest,1n),1n+rest,WordEncoding.concat(rest,1n,tail,Word.zero(1n)),
114	                Addition.successor_width(rest))},
115	            WCon{bit,Word.shr.pad(rest,tail)},
116	            WordWidth.transport_cons(Nat.add(rest,1n),1n+rest,bit,WordEncoding.concat(rest,1n,tail,Word.zero(1n)),
117	              Addition.successor_width(rest)),
118	            Equal.cong(Word(1n+rest),Word(2n+rest),w => WCon{bit,w},WordWidth.transport(Nat.add(rest,1n),1n+rest,WordEncoding.concat(rest,1n,
119	                  tail,Word.zero(1n)),Addition.successor_width(rest)),Word.shr.pad(rest,tail),concat_pad(rest,tail)))
120	
121	def padded_successor(+low: Word(31n)) -> {U32.to_nat(U32.add(U32{Word.shr.pad(31n,low)},1)) == 1n+U32.to_nat(U32{Word.shr.pad(31n,low)}) : Nat}:
122	  %Equal.sym(Word(32n),Word.add(32n,Word.shr.pad(31n,low),Word.inc(32n,Word.zero(32n))),Word.inc(32n,Word.shr.pad(31n,low)),add_one(32n,
123	      Word.shr.pad(31n,low))) : {Word.to_nat(32n,_) == 1n+Word.to_nat(32n,Word.shr.pad(31n,low)) : Nat}
124	  %Equal.sym(Nat,Word.to_nat(32n,Word.shr.pad(31n,low)),Word.to_nat(31n,low),pad_nat(31n,low)) : {Word.to_nat(32n,Word.inc(32n,Word.shr.pad(31n,
125	          low))) == 1n+_ : Nat}
126	  inc_nat(31n,low)
127	
128	def Goal(+i: U32) -> Type:
129	  {U32.is_lt(i,2147483648) == True{} : Bool} -> {U32.to_nat((i + 1 : U32)) == 1n+U32.to_nat(i) : Nat}
130	
131	def parts(+parts: WordEncoding.Split<31n,1n>) -> Goal(U32{WordEncoding.join(31n,1n,parts)}):
132	  WordEncoding.Parts{+low,+high} = parts
133	  bound =>
134	    %Equal.sym(Word(1n),high,Word.zero(1n),WordEncoding.upper_zero(31n,0n,low,high,bound)) : {U32.to_nat(U32.add(U32{WordEncoding.concat(31n,1n,
135	            low,_)},1)) == 1n+U32.to_nat(U32{WordEncoding.concat(31n,1n,low,_)}) : Nat}
136	    %Equal.sym(Word(32n),WordEncoding.concat(31n,1n,low,Word.zero(1n)),Word.shr.pad(31n,low),concat_pad(31n,low)) : {U32.to_nat(U32.add(U32{_},
137	          1)) == 1n+U32.to_nat(U32{_}) : Nat}
138	    padded_successor(low)
139	
140	def word(+w: Word(32n)) -> Goal(U32{w}):
141	  %WordEncoding.recover(31n,1n,w) : Goal(U32{_})
142	  parts(WordEncoding.split(31n,1n,w))
143	
144	law successor:
145	  for +i: U32
146	  Goal(i)
147	def successor(i):
148	  match i:
149	    case U32{w}:
150	      word(w)