def mask_word

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

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

358def mask_word(+m: Nat, +k: Nat, +w: Word(m), h: {Nat.is_lt(Word.to_nat(m, w), Model.capacity(k)) == True{} : Bool}) ->
359  {w == Word.and(m, w, low(m, k)) : Word(m)}:
360  match m:
361    case 0n:
362      match w:
363        case WNil{}:
364          {==}
365    case 1n+q:
366      match k:
367        case 0n:
368          match w:
369            case WCon{+b, +t}:
370              match b:
371                case False{}:
372                  %mask_word(q, 0n, t, lt_d1(Word.to_nat(q, t), h)) : {WCon{False{}, t} == WCon{False{}, _} : Word(1n+q)}
373                  {==}
374                case True{}:
375                  Empty.absurd({WCon{True{}, t} == Word.and(1n+q, WCon{True{}, t}, low(1n+q, 0n)) : Word(1n+q)}, lt_zero(Nat.double(Word.to_nat(q, t)), h))
376        case 1n+r:
377          match w:
378            case WCon{+b, +t}:
379              match b:
380                case False{}:
381                  %mask_word(q, r, t, lt_half(False{}, Word.to_nat(q, t), r, h)) : {WCon{False{}, t} == WCon{False{}, _} : Word(1n+q)}
382                  {==}
383                case True{}:
384                  %mask_word(q, r, t, lt_half(True{}, Word.to_nat(q, t), r, h)) : {WCon{True{}, t} == WCon{True{}, _} : Word(1n+q)}
385                  {==}