F64bits.xtop: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend as F64bits
Lines 91-104 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend&start_line=91&end_line=104

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

def xtop(+p: Nat, +w: Word(1n+p)) -> {S.unsigned(1n+p, Word.xor(1n+p, w, WD.pw(1n+p, p))) == Nat.add(C.low(p, S.unsigned(1n+p, w)), C.shift(p, Nat.sub(1n, C.high(p, S.unsigned(1n+p, w))))) : Nat}:
  match p:
    case 0n:
      match w:
        case WCon{+b, +t}:
          match b:
            case True{}:
              {==}
            case False{}:
              {==}
    case 1n+ +q:
      match w:
        case WCon{+b, +t}:
          xstep(q, b, t, xtop(q, t))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=pw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend&name=xstep
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift