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	
7	def predecessor_strict(+a: Nat,+b: Nat,h: {Nat.is_le(1n+a,b) == True{} : Bool}) -> {Nat.is_lt(a,b) == True{} : Bool}:
8	  match a b:
9	    case 0n 0n:
10	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(h))
11	    case 0n 1n+bp:
12	      {==}
13	    case 1n+ap 0n:
14	      Empty.absurd({Nat.is_lt(1n+ap,0n) == True{} : Bool},WordEncoding.false_true(h))
15	    case 1n+ap 1n+bp:
16	      predecessor_strict(ap,bp,h)
17	
18	def strict_le(+a: Nat,+b: Nat,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_le(a,b) == True{} : Bool}:
19	  match a b:
20	    case 0n 0n:
21	      {==}
22	    case 0n 1n+bp:
23	      {==}
24	    case 1n+ap 0n:
25	      Empty.absurd({Nat.is_le(1n+ap,0n) == True{} : Bool},WordEncoding.false_true(h))
26	    case 1n+ap 1n+bp:
27	      strict_le(ap,bp,h)
28	
29	def add_one(+i: U32) -> {U32.add(i,1) == U32.inc(i) : U32}:
30	  match i:
31	    case U32{+w}:
32	      %U32Successor.add_one(32n,w) : {U32{Word.add(32n,w,Word.inc(32n,Word.zero(32n)))} == U32{_} : U32}
33	      {==}
34	
35	def native_bound(+n: Nat,+cap: U32,e: {U32.to_nat(U32.from_nat(n)) == n : Nat},h: {Nat.is_lt(n,
36	      U32.to_nat(cap)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(n),cap) == True{} : Bool}:
37	  %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),
38	      cap)) : {_ == True{} : Bool}
39	  %Equal.sym(Nat,U32.to_nat(U32.from_nat(n)),n,e) : {Nat.is_lt(_,U32.to_nat(cap)) == True{} : Bool}
40	  h
41	
42	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,
43	    c) == True{} : Bool}:
44	  match a b c:
45	    case 0n 0n c:
46	      Empty.absurd({Nat.is_lt(0n,c) == True{} : Bool},WordEncoding.false_true(ab))
47	    case 0n 1n+b 0n:
48	      Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
49	    case 0n 1n+b 1n+c:
50	      {==}
51	    case 1n+a 0n c:
52	      Empty.absurd({Nat.is_lt(1n+a,c) == True{} : Bool},WordEncoding.false_true(ab))
53	    case 1n+a 1n+b 0n:
54	      Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(bc))
55	    case 1n+a 1n+b 1n+c:
56	      nat_trans(a,b,c,ab,bc)
57	
58	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}:
59	  %Comparison.lt(a,b) : {_ == True{} : Bool}
60	  h
61	
62	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}:
63	  %Comparison.le(a,b) : {_ == True{} : Bool}
64	  h
65	
66	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,
67	    c) == True{} : Bool}:
68	  %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}
69	  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))
70	
71	law roundtrip:
72	  for +n: Nat
73	  for +cap: U32
74	  for +cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool}
75	  for h: {Nat.is_le(n,U32.to_nat(cap)) == True{} : Bool}
76	  {U32.to_nat(U32.from_nat(n)) == n : Nat}
77	def roundtrip(n,cap,cap_ok,h):
78	  match n:
79	    case 0n:
80	      {==}
81	    case 1n+ +p:
82	      +small = predecessor_strict(p,U32.to_nat(cap),h)
83	      +previous = roundtrip(p,cap,cap_ok,strict_le(p,U32.to_nat(cap),small))
84	      %previous : {U32.to_nat(U32.inc(U32.from_nat(p))) == 1n+_ : Nat}
85	      %add_one(U32.from_nat(p)) : {U32.to_nat(_) == 1n+U32.to_nat(U32.from_nat(p)) : Nat}
86	      U32Successor.successor(U32.from_nat(p))(uint_trans(U32.from_nat(p),cap,2147483648,native_bound(p,cap,previous,small),cap_ok))