def cmp_bits

bendtorch-core@0.1.0.0 · src/storage/arith.bend:73

import Base

73def cmp_bits(+x: Nat, +y: Nat, +a: Bool, +b: Bool) ->
74  {Word.cmp.fin(a, b, Nat.cmp(x, y)) == Nat.cmp(bit(a, x), bit(b, y)) : Cmp}:
75  match x y:
76    case 0n 0n:
77      match a b:
78        case False{} False{}:
79          {==}
80        case False{} True{}:
81          {==}
82        case True{} False{}:
83          {==}
84        case True{} True{}:
85          {==}
86    case 0n 1n+q:
87      match a b:
88        case False{} False{}:
89          {==}
90        case False{} True{}:
91          {==}
92        case True{} False{}:
93          {==}
94        case True{} True{}:
95          {==}
96    case 1n+p 0n:
97      match a b:
98        case False{} False{}:
99          {==}
100        case False{} True{}:
101          {==}
102        case True{} False{}:
103          {==}
104        case True{} True{}:
105          {==}
106    case 1n+p 1n+q:
107      match a b:
108        case False{} False{}:
109          cmp_bits(p, q, False{}, False{})
110        case False{} True{}:
111          cmp_bits(p, q, False{}, True{})
112        case True{} False{}:
113          cmp_bits(p, q, True{}, False{})
114        case True{} True{}:
115          cmp_bits(p, q, True{}, True{})