1	# Exact conversions over the complete U32 range. Tensor stride-zero extents may
2	# exceed the physical array capacity, so storage-capacity bounds are insufficient.
3	import Base
4	import ./nat_order.bend as Order
5	import ./u32_successor.bend as U32Successor
6	import ./nat_to_u32_bounds.bend as Bounds
7	import ./word_encoding.bend as WordEncoding
8	import ./bounded_u32_arithmetic.bend as Arithmetic
9	import ./word_multiplication.bend as Multiplication
10	
11	def ones(width: Nat) -> Word(width):
12	  match width:
13	    case 0n: WNil{}
14	    case 1n+rest: WCon{True{},ones(rest)}
15	
16	def equal_low_less(+comparison: Cmp) -> {Cmp.is_lt(Word.cmp.fin(True{},True{},comparison)) == Cmp.is_lt(comparison) : Bool}:
17	  match comparison:
18	    case LT{}: {==}
19	    case EQ{}: {==}
20	    case GT{}: {==}
21	
22	def finish_bounded(+bit: Bool,+comparison: Cmp,ordered: {Cmp.is_le(comparison) == True{} : Bool}) ->
23	  {Cmp.is_le(Word.cmp.fin(bit,True{},comparison)) == True{} : Bool}:
24	  match bit comparison:
25	    case False{} LT{}: {==}
26	    case False{} EQ{}: {==}
27	    case False{} GT{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(ordered))
28	    case True{} LT{}: {==}
29	    case True{} EQ{}: {==}
30	    case True{} GT{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(ordered))
31	
32	def bounded(+width: Nat,+word: Word(width)) -> {Cmp.is_le(Word.cmp(width,word,ones(width))) == True{} : Bool}:
33	  match width:
34	    case 0n: {==}
35	    case 1n+ +rest:
36	      WCon{bit,+tail} = word
37	      finish_bounded(bit,Word.cmp(rest,tail,ones(rest)),bounded(rest,tail))
38	
39	def increment(+width: Nat,+word: Word(width),below: {Cmp.is_lt(Word.cmp(width,word,ones(width))) == True{} : Bool}) ->
40	  {Word.to_nat(width,Word.inc(width,word)) == 1n+Word.to_nat(width,word) : Nat}:
41	  match width:
42	    case 0n: Empty.absurd({0n == 1n : Nat},WordEncoding.false_true(below))
43	    case 1n+ +rest:
44	      match word:
45	        case WCon{False{},tail}: {==}
46	        case WCon{True{},+tail}:
47	          %increment(rest,tail,{
48	            %equal_low_less(Word.cmp(rest,tail,ones(rest))) : {_ == True{} : Bool}
49	            below : {Cmp.is_lt(Word.cmp(rest,tail,ones(rest))) == True{} : Bool}}) :
50	            {Nat.double(Word.to_nat(rest,Word.inc(rest,tail))) == Nat.double(_) : Nat}
51	          {==}
52	
53	def maximum(+value: U32) -> {U32.is_le(value,4294967295) == True{} : Bool}:
54	  U32{+word} = value
55	  bounded(32n,word)
56	
57	def successor(+value: U32,below: {U32.is_lt(value,4294967295) == True{} : Bool}) ->
58	  {U32.to_nat(U32.add(value,1)) == 1n+U32.to_nat(value) : Nat}:
59	  U32{+word} = value
60	  %Equal.sym(Word(32n),Word.add(32n,word,Word.inc(32n,Word.zero(32n))),Word.inc(32n,word),U32Successor.add_one(32n,word)) :
61	    {Word.to_nat(32n,_) == 1n+Word.to_nat(32n,word) : Nat}
62	  increment(32n,word,below)
63	
64	def roundtrip(+value: Nat,+capacity: U32,inside: {Nat.is_le(value,U32.to_nat(capacity)) == True{} : Bool}) ->
65	  {U32.to_nat(U32.from_nat(value)) == value : Nat}:
66	  match value:
67	    case 0n: {==}
68	    case 1n+ +previous:
69	      +below = Bounds.predecessor_strict(previous,U32.to_nat(capacity),inside)
70	      +exact = roundtrip(previous,capacity,Bounds.strict_le(previous,U32.to_nat(capacity),below))
71	      %exact : {U32.to_nat(U32.inc(U32.from_nat(previous))) == 1n+_ : Nat}
72	      %Bounds.add_one(U32.from_nat(previous)) : {U32.to_nat(_) == 1n+U32.to_nat(U32.from_nat(previous)) : Nat}
73	      successor(U32.from_nat(previous),Bounds.uint_trans(U32.from_nat(previous),capacity,4294967295,
74	        Bounds.native_bound(previous,capacity,exact,below),maximum(capacity)))
75	
76	def add(+left: U32,+right: U32,+capacity: U32,
77	  inside: {Nat.is_le(Nat.add(U32.to_nat(left),U32.to_nat(right)),U32.to_nat(capacity)) == True{} : Bool}) ->
78	  {U32.to_nat(U32.add(left,right)) == Nat.add(U32.to_nat(left),U32.to_nat(right)) : Nat}:
79	  %Equal.sym(U32,U32.add(left,right),U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))),Arithmetic.native_add(left,right)) :
80	    {U32.to_nat(_) == Nat.add(U32.to_nat(left),U32.to_nat(right)) : Nat}
81	  roundtrip(Nat.add(U32.to_nat(left),U32.to_nat(right)),capacity,inside)
82	
83	def subtract(+left: U32,+right: U32,+capacity: U32,
84	  ordered: {Nat.is_le(U32.to_nat(right),U32.to_nat(left)) == True{} : Bool},
85	  inside: {Nat.is_le(Nat.sub(U32.to_nat(left),U32.to_nat(right)),U32.to_nat(capacity)) == True{} : Bool}) ->
86	  {U32.to_nat(U32.sub(left,right)) == Nat.sub(U32.to_nat(left),U32.to_nat(right)) : Nat}:
87	  %Equal.sym(U32,U32.sub(left,right),U32.from_nat(Nat.sub(U32.to_nat(left),U32.to_nat(right))),Arithmetic.native_subtract(left,right,ordered)) :
88	    {U32.to_nat(_) == Nat.sub(U32.to_nat(left),U32.to_nat(right)) : Nat}
89	  roundtrip(Nat.sub(U32.to_nat(left),U32.to_nat(right)),capacity,inside)
90	
91	def multiply(+left: U32,+right: U32,+capacity: U32,
92	  inside: {Nat.is_le(Nat.mul(U32.to_nat(left),U32.to_nat(right)),U32.to_nat(capacity)) == True{} : Bool}) ->
93	  {U32.to_nat(U32.mul(left,right)) == Nat.mul(U32.to_nat(left),U32.to_nat(right)) : Nat}:
94	  %Equal.sym(U32,U32.mul(left,right),U32.from_nat(Nat.mul(U32.to_nat(left),U32.to_nat(right))),Multiplication.native_multiply(left,right)) :
95	    {U32.to_nat(_) == Nat.mul(U32.to_nat(left),U32.to_nat(right)) : Nat}
96	  roundtrip(Nat.mul(U32.to_nat(left),U32.to_nat(right)),capacity,inside)
97	
98	# Subtracting a common interval origin preserves its strict upper bound.
99	def interval_inside(+low: U32,+high: U32,+position: U32,
100	  +lower: {U32.is_le(low,position) == True{} : Bool},+upper: {U32.is_lt(position,high) == True{} : Bool}) ->
101	  {Nat.is_lt(U32.to_nat((position - low : U32)),U32.to_nat((high - low : U32))) == True{} : Bool}:
102	  +ln = U32.to_nat(low)
103	  +hn = U32.to_nat(high)
104	  +pn = U32.to_nat(position)
105	  +ordered = Bounds.as_nat_le(low,position,lower)
106	  +before = Bounds.as_nat_lt(position,high,upper)
107	  +low_high = Order.le_lt_trans(ln,pn,hn,ordered,before)
108	  +local = Nat.sub(pn,ln)
109	  +relative_exact = subtract(position,low,position,ordered,Order.sub_le(pn,ln))
110	  +range_exact = subtract(high,low,high,Bounds.strict_le(ln,hn,low_high),Order.sub_le(hn,ln))
111	  %Equal.sym(Nat,U32.to_nat((position - low : U32)),local,relative_exact) : {Nat.is_lt(_,U32.to_nat((high - low : U32))) == True{} : Bool}
112	  %Equal.sym(Nat,U32.to_nat((high - low : U32)),Nat.sub(hn,ln),range_exact) : {Nat.is_lt(local,_) == True{} : Bool}
113	  %Equal.sym(Bool,Nat.is_lt(local,Nat.sub(hn,ln)),Nat.is_lt(Nat.add(ln,local),hn),Order.subtraction_lt(hn,ln,local)) : {_ == True{} : Bool}
114	  %Equal.sym(Nat,Nat.add(ln,local),pn,Order.restore_shift(ln,pn,ordered)) : {Nat.is_lt(_,hn) == True{} : Bool} before