1	# Safe Nat -> U32 -> Nat conversion over the candidate's finite envelope.
2	import Base
3	import ./u32_successor.bend as U32Successor
4	import ./u32_comparison.bend as Comparison
5	import ./word_encoding.bend as WordEncoding
6	import ./natural_addition.bend as Addition
7	import ./word_arithmetic.bend as WordArithmetic
8	
9	def predecessor_strict(+a: Nat,+b: Nat,h: {Nat.is_le(1n+a,b) == True{} : Bool}) -> {Nat.is_lt(a,b) == True{} : Bool}:
10	  match a b:
11	    case 0n 0n:
12	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(h))
13	    case 0n 1n+bp:
14	      {==}
15	    case 1n+ap 0n:
16	      Empty.absurd({Nat.is_lt(1n+ap,0n) == True{} : Bool},WordEncoding.false_true(h))
17	    case 1n+ap 1n+bp:
18	      predecessor_strict(ap,bp,h)
19	
20	def strict_le(+a: Nat,+b: Nat,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_le(a,b) == True{} : Bool}:
21	  match a b:
22	    case 0n 0n:
23	      {==}
24	    case 0n 1n+bp:
25	      {==}
26	    case 1n+ap 0n:
27	      Empty.absurd({Nat.is_le(1n+ap,0n) == True{} : Bool},WordEncoding.false_true(h))
28	    case 1n+ap 1n+bp:
29	      strict_le(ap,bp,h)
30	
31	def add_one(+i: U32) -> {U32.add(i,1) == U32.inc(i) : U32}:
32	  match i:
33	    case U32{+w}:
34	      %U32Successor.add_one(32n,w) : {U32{Word.add(32n,w,Word.inc(32n,Word.zero(32n)))} == U32{_} : U32}
35	      {==}
36	
37	def native_bound(+n: Nat,+cap: U32,e: {U32.to_nat(U32.from_nat(n)) == n : Nat},h: {Nat.is_lt(n,
38	      U32.to_nat(cap)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(n),cap) == True{} : Bool}:
39	  %Equal.sym(Bool,U32.is_lt(U32.from_nat(n),cap),Nat.is_lt(U32.to_nat(U32.from_nat(n)),U32.to_nat(cap)),Comparison.lt(U32.from_nat(n),
40	      cap)) : {_ == True{} : Bool}
41	  %Equal.sym(Nat,U32.to_nat(U32.from_nat(n)),n,e) : {Nat.is_lt(_,U32.to_nat(cap)) == True{} : Bool}
42	  h
43	
44	def nat_trans(+a: Nat,+b: Nat,+c: Nat,ab: {Nat.is_lt(a,b) == True{} : Bool},bc: {Nat.is_le(b,c) == True{} : Bool}) -> {Nat.is_lt(a,
45	    c) == True{} : Bool}:
46	  match a b c:
47	    case 0n 0n c:
48	      Empty.absurd({Nat.is_lt(0n,c) == True{} : Bool},WordEncoding.false_true(ab))
49	    case 0n 1n+b 0n:
50	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
51	    case 0n 1n+b 1n+c:
52	      {==}
53	    case 1n+a 0n c:
54	      Empty.absurd({Nat.is_lt(1n+a,c) == True{} : Bool},WordEncoding.false_true(ab))
55	    case 1n+a 1n+b 0n:
56	      Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(bc))
57	    case 1n+a 1n+b 1n+c:
58	      nat_trans(a,b,c,ab,bc)
59	
60	def as_nat_lt(+a: U32,+b: U32,h: {U32.is_lt(a,b) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(a),U32.to_nat(b)) == True{} : Bool}:
61	  %Comparison.lt(a,b) : {_ == True{} : Bool}
62	  h
63	
64	def as_nat_le(+a: U32,+b: U32,h: {U32.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(U32.to_nat(a),U32.to_nat(b)) == True{} : Bool}:
65	  %Comparison.le(a,b) : {_ == True{} : Bool}
66	  h
67	
68	def uint_trans(+a: U32,+b: U32,+c: U32,ab: {U32.is_lt(a,b) == True{} : Bool},bc: {U32.is_le(b,c) == True{} : Bool}) -> {U32.is_lt(a,
69	    c) == True{} : Bool}:
70	  %Equal.sym(Bool,U32.is_lt(a,c),Nat.is_lt(U32.to_nat(a),U32.to_nat(c)),Comparison.lt(a,c)) : {_ == True{} : Bool}
71	  nat_trans(U32.to_nat(a),U32.to_nat(b),U32.to_nat(c),as_nat_lt(a,b,ab),as_nat_le(b,c,bc))
72	
73	law roundtrip:
74	  for +n: Nat
75	  for +cap: U32
76	  for +cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool}
77	  for h: {Nat.is_le(n,U32.to_nat(cap)) == True{} : Bool}
78	  {U32.to_nat(U32.from_nat(n)) == n : Nat}
79	def roundtrip(n,cap,cap_ok,h):
80	  match n:
81	    case 0n:
82	      {==}
83	    case 1n+ +p:
84	      +small = predecessor_strict(p,U32.to_nat(cap),h)
85	      +previous = roundtrip(p,cap,cap_ok,strict_le(p,U32.to_nat(cap),small))
86	      %previous : {U32.to_nat(U32.inc(U32.from_nat(p))) == 1n+_ : Nat}
87	      %add_one(U32.from_nat(p)) : {U32.to_nat(_) == 1n+U32.to_nat(U32.from_nat(p)) : Nat}
88	      U32Successor.successor(U32.from_nat(p))(uint_trans(U32.from_nat(p),cap,2147483648,native_bound(p,cap,previous,small),cap_ok))
89	
90	def increment_encoded(+position: Nat) -> {(U32.from_nat(position) + 1 : U32) == U32.from_nat(1n+position) : U32}:
91	  %Addition.successor_width(position) : {(U32.from_nat(position) + 1 : U32) == U32.from_nat(_) : U32}
92	  WordArithmetic.native_add(position,1n)