1	import Base
2	import ../spec/numeric.bend as S
3	import ./numeric.bend as N
4	
5	# Base compares high bits first. Mathematical interpretation preserves that
6	# exact comparison, including equality, at every width.
7	def digits(a: Nat, b: Nat, x: Bool, y: Bool) -> {Nat.cmp(Nat.add(S.bit_value(x), Nat.double(a)), Nat.add(S.bit_value(y), Nat.double(b))) == Word.cmp.fin(x, y, Nat.cmp(a, b)) : Cmp}:
8	  match a b:
9	    case 0n 0n:
10	      match x y:
11	        case False{} False{}: {==}
12	        case False{} True{}: {==}
13	        case True{} False{}: {==}
14	        case True{} True{}: {==}
15	    case 0n 1n+p:
16	      match x y:
17	        case False{} False{}: {==}
18	        case False{} True{}: {==}
19	        case True{} False{}: {==}
20	        case True{} True{}: {==}
21	    case 1n+p 0n:
22	      match x y:
23	        case False{} False{}: {==}
24	        case False{} True{}: {==}
25	        case True{} False{}: {==}
26	        case True{} True{}: {==}
27	    case 1n+p 1n+q:
28	      match x y:
29	        case False{} False{}: digits(p, q, False{}, False{})
30	        case False{} True{}: digits(p, q, False{}, True{})
31	        case True{} False{}: digits(p, q, True{}, False{})
32	        case True{} True{}: digits(p, q, True{}, True{})
33	
34	def refines(+n: Nat, a: Word(n), b: Word(n)) -> {Word.cmp(n, a, b) == Nat.cmp(S.unsigned(n, a), S.unsigned(n, b)) : Cmp}:
35	  match n:
36	    case 0n:
37	      match a b:
38	        case WNil{} WNil{}: {==}
39	    case 1n+ +p:
40	      match a b:
41	        case WCon{+x, +at} WCon{+y, +bt}:
42	          Equal.trans(Cmp, Word.cmp.fin(x, y, Word.cmp(p, at, bt)), Word.cmp.fin(x, y, Nat.cmp(S.unsigned(p, at), S.unsigned(p, bt))), Nat.cmp(Nat.add(S.bit_value(x), Nat.double(S.unsigned(p, at))), Nat.add(S.bit_value(y), Nat.double(S.unsigned(p, bt)))), Equal.cong(Cmp, Cmp, c => Word.cmp.fin(x, y, c), Word.cmp(p, at, bt), Nat.cmp(S.unsigned(p, at), S.unsigned(p, bt)), refines(p, at, bt)), Equal.sym(Cmp, Nat.cmp(Nat.add(S.bit_value(x), Nat.double(S.unsigned(p, at))), Nat.add(S.bit_value(y), Nat.double(S.unsigned(p, bt)))), Word.cmp.fin(x, y, Nat.cmp(S.unsigned(p, at), S.unsigned(p, bt))), digits(S.unsigned(p, at), S.unsigned(p, bt), x, y)))
43	
44	def u32_refines(a: U32, b: U32) -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}:
45	  match a b:
46	    case U32{+x} U32{+y}:
47	      %Equal.sym(Nat, Word.to_nat(32n, x), S.unsigned(32n, x), N.primitive_word_interpretation(32n, x)) : {U32.cmp(U32{x}, U32{y}) == Nat.cmp(_, Word.to_nat(32n, y)) : Cmp}
48	      %Equal.sym(Nat, Word.to_nat(32n, y), S.unsigned(32n, y), N.primitive_word_interpretation(32n, y)) : {U32.cmp(U32{x}, U32{y}) == Nat.cmp(S.unsigned(32n, x), _) : Cmp}
49	      refines(32n, x, y)
50	
51	def u32_ge(+a: U32, +b: U32) -> {U32.is_ge(a, b) == Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) : Bool}:
52	  Equal.cong(Cmp, Bool, Cmp.is_ge, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_refines(a, b))
53	
54	def u32_lt(+a: U32, +b: U32) -> {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}:
55	  Equal.cong(Cmp, Bool, Cmp.is_lt, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_refines(a, b))