def sub_word

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

import Base

188# Word.sub(a, b) is Word.adc(a, b, True, True): it adds the complement of b
189# with an incoming carry, so a cleared carry is a borrow of one.
190def sub_word(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool,
191  h: {Nat.is_le(Nat.add(borrow(c), Word.to_nat(n, b)), Word.to_nat(n, a)) == True{} : Bool}) ->
192  {Nat.add(borrow(c), Nat.add(Word.to_nat(n, b), Word.to_nat(n, Word.adc(n, a, b, True{}, c)))) == Word.to_nat(n, a) : Nat}:
193  match n:
194    case 0n:
195      match c:
196        case False{}:
197          Empty.absurd({1n == 0n : Nat}, clash(h))
198        case True{}:
199          {==}
200    case 1n+p:
201      match a:
202        case WCon{+x, +xs}:
203          match x:
204            case False{}:
205              match b:
206                case WCon{+y, +ys}:
207                  match y:
208                    case False{}:
209                      match c:
210                        case False{}:
211                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
212                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
213                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+_ : Nat}
214                          {==}
215                        case True{}:
216                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == Nat.double(_) : Nat}
217                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == _ : Nat}
218                          {==}
219                    case True{}:
220                      match c:
221                        case False{}:
222                          %sub_word(p, xs, ys, False{}, le_dd(1n+Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
223                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
224                          {==}
225                        case True{}:
226                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
227                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
228                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+_ : Nat}
229                          {==}
230            case True{}:
231              match b:
232                case WCon{+y, +ys}:
233                  match y:
234                    case False{}:
235                      match c:
236                        case False{}:
237                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
238                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
239                          {==}
240                        case True{}:
241                          %sub_word(p, xs, ys, True{}, le_ds(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
242                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
243                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == _ : Nat}
244                          {==}
245                    case True{}:
246                      match c:
247                        case False{}:
248                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+Nat.double(_) : Nat}
249                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 3n+_ : Nat}
250                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
251                          {==}
252                        case True{}:
253                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
254                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
255                          {==}