~/jendhub

def uq.pad

bend-osdev-algo@0.1.0.0 · proof_u32.bend:535

import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
import Base

535# padding a word with a zero top bit keeps its value
536def uq.pad(p: Nat, t: Word(p)) -> {Word.to_nat(1n+p, Word.shr.pad(p, t)) == Word.to_nat(p, t) : Nat}:
537  match p:
538    case 0n:
539      {==}
540    case 1n+ +q:
541      match t:
542        case WCon{False{}, +r}:
543          uq.double_cong(Word.to_nat(1n+q, Word.shr.pad(q, r)), Word.to_nat(q, r), uq.pad(q, r))
544        case WCon{True{}, +r}:
545          uq.succ_cong(Nat.double(Word.to_nat(1n+q, Word.shr.pad(q, r))), Nat.double(Word.to_nat(q, r)), uq.double_cong(Word.to_nat(1n+q, Word.shr.pad(q, r)), Word.to_nat(q, r), uq.pad(q, r)))

Uses (9)

Used by (1)