Word-RAM interface for indexed min-priority queues

This file packages uniform Word-RAM calling conventions (PQCode) and parametric specification / resource certificates (PQPackage) for Cslib.Algorithms.Lean.IndexedMinPQ.spec.

A PQPackage B r_pq bundles a SubroutineCode B r_pq 1 with:

• three 1-bit operation-tag registers (tag2, tag1, tag0) taking values only in {0, 1}, so encoded operation arguments fit in w-bit words even at small word sizes (w ≥ 1);
• standard argument registers (argV, argK) and result registers (outFlag, outV, outK);
• parametric SubroutineDS certificates over (n, K_max, w, base) supporting arbitrary concrete potentials potential : Data r_pq → ℕ (both worst-case potential = 0 heaps such as BinaryHeap and amortized heaps such as FibonacciHeap).

It also provides basis-polymorphic inline caller helpers (callIsEmpty, callGetKey, callInsert, callDecreaseKey, callExtractMin) built from Op.copy and SubroutineDS.call_rename.

Main definitions

• Cslib.Algorithms.WordRAM.PriorityQueue.PQCode: SubroutineCode B r_pq 1 equipped with standard priority-queue interface registers, encode, argMatch, decode, and inline caller blocks.
• Cslib.Algorithms.WordRAM.PriorityQueue.PQPackage: uniform code together with parametric SubroutineDS certificates and per-operation amortized charge bounds.

Main results

• PQCode.arguments_fit, PQCode.encode_matches: generic proof that the standard priority-queue encoding fits in w-bit words and satisfies argMatch.
• PQCode.callIsEmpty_exec, PQCode.callGetKey_exec, PQCode.callInsert_exec, PQCode.callDecreaseKey_exec, PQCode.callExtractMin_exec: relocated inline operation calls with amortized potential accounting and bidirectional framing.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms

PQCode: Uniform priority-queue subroutine code and calling convention

structure Cslib.Algorithms.WordRAM.PriorityQueue.PQCode (B : WordRAM.Basis) (r_pq : ℕ) extends Cslib.WordRAM.SubroutineCode B r_pq 1 : Type

Uniform machine code and register calling convention for an indexed min-priority queue over basis B using r_pq local registers.

• allocSpan : Code B r_pq
• initSetup : Code B r_pq
• code : Code B r_pq
• frontierReg : Fin r_pq
• baseReg : Fin r_pq
• initParams : Fin 1 → Fin r_pq
• curReg : Fin r_pq
• zeroReg : Fin r_pq
• oneReg : Fin r_pq
• incCur : Op B r_pq
• input : Fin r_pq → Bool
• output : Fin r_pq
• nReg : Fin r_pq

  Register holding the handle-universe size n at initialization (initParams = ![nReg]).

• tag2 : Fin r_pq

  High tag bit (≠ 0 selects extractMin).

• tag1 : Fin r_pq

  Middle tag bit (≠ 0 selects insert / decreaseKey when tag2 = 0).

• tag0 : Fin r_pq

  Low tag bit (0 selects isEmpty / insert; ≠ 0 selects getKey / decreaseKey).

• argV : Fin r_pq

  Handle argument register (v.val for getKey, insert, decreaseKey).

• argK : Fin r_pq

  Key argument register (k for insert, decreaseKey).

• outFlag : Fin r_pq

  Flag output register (1/0 for isEmpty, getKey, extractMin).

• outV : Fin r_pq

  Extracted handle output register (u.val for non-empty extractMin).

• outK : Fin r_pq

  Key output register (k for present getKey and non-empty extractMin).

• initParams_eq : self.initParams = ![self.nReg]

  Initialization takes n in nReg.

• nReg_ne_frontier : self.nReg ≠ self.frontierReg

  nReg is distinct from frontierReg so callers can pass n and frontier together.

• args_nodup : [self.tag2, self.tag1, self.tag0, self.argV, self.argK].Nodup

  Tag and argument registers are pairwise distinct.

• tag2_input : self.input self.tag2 = true

  tag2 is a caller-overwritable input register.

• tag1_input : self.input self.tag1 = true

  tag1 is a caller-overwritable input register.

• tag0_input : self.input self.tag0 = true

  tag0 is a caller-overwritable input register.

• argV_input : self.input self.argV = true

  argV is a caller-overwritable input register.

• argK_input : self.input self.argK = true

  argK is a caller-overwritable input register.

• output_eq : self.output = self.outFlag

  Primary halting output register is outFlag.

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.mapSimulates {B B' : WordRAM.Basis} {r_pq : ℕ} (φ : B.Simulates B') (P : PQCode B r_pq) : PQCode B' r_pq

Translate a PQCode bundle along a basis simulation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.toStandard {r_pq : ℕ} (P : PQCode WordRAM.Basis.exact r_pq) : PQCode WordRAM.Basis.standard r_pq

Lift an exact-basis PQCode to Basis.standard.

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.encode {B : WordRAM.Basis} {r_pq : ℕ} (P : PQCode B r_pq) {n : ℕ} : Lean.IndexedMinPQ.Op n → Fin r_pq → ℕ

Standard register encoding for IndexedMinPQ.Op n using 1-bit tags (tag2, tag1, tag0).

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.argMatch {B : WordRAM.Basis} {r_pq : ℕ} (P : PQCode B r_pq) {n : ℕ} : Lean.IndexedMinPQ.Op n → (Fin r_pq → ℕ) → Prop

Partial argument-matching predicate for inline priority-queue calls.

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.decode {B : WordRAM.Basis} {r_pq : ℕ} (P : PQCode B r_pq) {n K_max : ℕ} (o : (Lean.IndexedMinPQ.spec n K_max).Op) : (Fin r_pq → ℕ) → Option ((Lean.IndexedMinPQ.spec n K_max).Result o)

Standard output decoder for IndexedMinPQ.spec n K_max.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.arguments_fit {B : WordRAM.Basis} {r_pq : ℕ} (P : PQCode B r_pq) {n K_max w base space : ℕ} (hsp : n + 1 ≤ space) (hS : WordRAM.Fits w (base + space)) (hK : WordRAM.Fits w K_max) {s : Lean.IndexedMinPQ.State n} (o : Lean.IndexedMinPQ.Op n) (hv : (Lean.IndexedMinPQ.spec n K_max).valid s o) (i : Fin r_pq) : WordRAM.Fits w (P.encode o i)

Standard encoded arguments fit in w-bit words whenever n + 1 ≤ space, Fits w (base + space), and Fits w K_max.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.encode_matches {B : WordRAM.Basis} {r_pq : ℕ} (P : PQCode B r_pq) {n : ℕ} (o : Lean.IndexedMinPQ.Op n) (regs : Fin r_pq → ℕ) : P.argMatch o fun (i : Fin r_pq) => if P.input i = true then P.encode o i else regs i

Full standalone prepare register delivery satisfies P.argMatch.

Basis-polymorphic inline caller blocks and execution lemmas

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callIsEmpty {B : WordRAM.Basis} {r_pq r_caller : ℕ} (P : PQCode B r_pq) (f : Fin r_pq → Fin r_caller) (zeroReg_c : Fin r_caller) : WordRAM.Code B r_caller

Relocated inline call to isEmpty, copying 0 from zeroReg_c.

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callExtractMin {B : WordRAM.Basis} {r_pq r_caller : ℕ} (P : PQCode B r_pq) (f : Fin r_pq → Fin r_caller) (oneReg_c : Fin r_caller) : WordRAM.Code B r_caller

Relocated inline call to extractMin, copying 1 from oneReg_c.

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callGetKey {B : WordRAM.Basis} {r_pq r_caller : ℕ} (P : PQCode B r_pq) (f : Fin r_pq → Fin r_caller) (zeroReg_c oneReg_c vReg_c : Fin r_caller) : WordRAM.Code B r_caller

Relocated inline call to getKey, copying 0, 1, and handle vReg_c.

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callInsert {B : WordRAM.Basis} {r_pq r_caller : ℕ} (P : PQCode B r_pq) (f : Fin r_pq → Fin r_caller) (zeroReg_c oneReg_c vReg_c kReg_c : Fin r_caller) : WordRAM.Code B r_caller

Relocated inline call to insert, copying 0, 1, handle vReg_c, and key kReg_c.

def Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callDecreaseKey {B : WordRAM.Basis} {r_pq r_caller : ℕ} (P : PQCode B r_pq) (f : Fin r_pq → Fin r_caller) (zeroReg_c oneReg_c vReg_c kReg_c : Fin r_caller) : WordRAM.Code B r_caller

Relocated inline call to decreaseKey, copying 0, 1, handle vReg_c, and key kReg_c.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callIsEmpty_exec {B : WordRAM.Basis} {r_pq r_caller : ℕ} {P : PQCode B r_pq} {n K_max w base : ℕ} (C : WordRAM.SubroutineDS P.toSubroutineCode (Lean.IndexedMinPQ.spec n K_max) w base ![n] (Lean.IndexedMinPQ.empty n)) (harg_eq : C.argMatch = P.argMatch) (hdec_eq : C.decode = P.decode) {f : Fin r_pq → Fin r_caller} (hf : Function.Injective f) {zeroReg_c : Fin r_caller} (hz_out : zeroReg_c ∉ Set.range f) {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data r_caller} (hr : C.rep s (WordRAM.Data.comap f x)) (hz0 : x.regs zeroReg_c = 0) : ∃ (z : WordRAM.Data r_caller) (t : ℕ), WordRAM.ExecWithin w (P.callIsEmpty f zeroReg_c) x z t ∧ (z.regs (f P.outFlag) = 0 ↔ Lean.IndexedMinPQ.dom s ≠ ∅) ∧ C.rep s (WordRAM.Data.comap f z) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem z.mem ∧ (∀ j ∉ Set.range f, z.regs j = x.regs j) ∧ t + C.potential (WordRAM.Data.comap f z) ≤ 3 + C.charge s Lean.IndexedMinPQ.Op.isEmpty + C.potential (WordRAM.Data.comap f x)

Inline execution of P.callIsEmpty: preserves abstract state s, sets z.regs (f P.outFlag) so z.regs (f P.outFlag) = 0 ↔ IndexedMinPQ.dom s ≠ ∅, and charges 3 + C.charge s .isEmpty.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callExtractMin_exec {B : WordRAM.Basis} {r_pq r_caller : ℕ} {P : PQCode B r_pq} {n K_max w base : ℕ} (C : WordRAM.SubroutineDS P.toSubroutineCode (Lean.IndexedMinPQ.spec n K_max) w base ![n] (Lean.IndexedMinPQ.empty n)) (hsp_pos : 1 ≤ C.space) (hS : WordRAM.Fits w (base + C.space)) (harg_eq : C.argMatch = P.argMatch) (hdec_eq : C.decode = P.decode) {f : Fin r_pq → Fin r_caller} (hf : Function.Injective f) {oneReg_c : Fin r_caller} {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data r_caller} (hr : C.rep s (WordRAM.Data.comap f x)) (ho1 : x.regs oneReg_c = 1) : ∃ (z : WordRAM.Data r_caller) (t : ℕ), WordRAM.ExecWithin w (P.callExtractMin f oneReg_c) x z t ∧ P.decode Lean.IndexedMinPQ.Op.extractMin (WordRAM.Data.comap f z).regs = some ((Lean.IndexedMinPQ.spec n K_max).step s Lean.IndexedMinPQ.Op.extractMin).2 ∧ C.rep ((Lean.IndexedMinPQ.spec n K_max).step s Lean.IndexedMinPQ.Op.extractMin).1 (WordRAM.Data.comap f z) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem z.mem ∧ (∀ j ∉ Set.range f, z.regs j = x.regs j) ∧ t + C.potential (WordRAM.Data.comap f z) ≤ 1 + C.charge s Lean.IndexedMinPQ.Op.extractMin + C.potential (WordRAM.Data.comap f x)

Inline execution of P.callExtractMin: extracts findMin s and charges 1 + C.charge s .extractMin.

theorem Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callInsert_exec {B : WordRAM.Basis} {r_pq r_caller : ℕ} {P : PQCode B r_pq} {n K_max w base : ℕ} (C : WordRAM.SubroutineDS P.toSubroutineCode (Lean.IndexedMinPQ.spec n K_max) w base ![n] (Lean.IndexedMinPQ.empty n)) (hsp : n + 1 ≤ C.space) (hS : WordRAM.Fits w (base + C.space)) (hK : WordRAM.Fits w K_max) (harg_eq : C.argMatch = P.argMatch) {f : Fin r_pq → Fin r_caller} (hf : Function.Injective f) {zeroReg_c oneReg_c vReg_c kReg_c : Fin r_caller} (hz_out : zeroReg_c ∉ Set.range f) (ho_out : oneReg_c ∉ Set.range f) (hv_out : vReg_c ∉ Set.range f) (hk_out : kReg_c ∉ Set.range f) {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data r_caller} {v : Fin n} {k : ℕ} (hr : C.rep s (WordRAM.Data.comap f x)) (hval : s v = none ∧ k ≤ K_max) (hz0 : x.regs zeroReg_c = 0) (ho1 : x.regs oneReg_c = 1) (hvv : x.regs vReg_c = ↑v) (hvk : x.regs kReg_c = k) : ∃ (z : WordRAM.Data r_caller) (t : ℕ), WordRAM.ExecWithin w (P.callInsert f zeroReg_c oneReg_c vReg_c kReg_c) x z t ∧ C.rep (Function.update s v (some k)) (WordRAM.Data.comap f z) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem z.mem ∧ (∀ j ∉ Set.range f, z.regs j = x.regs j) ∧ t + C.potential (WordRAM.Data.comap f z) ≤ 5 + C.charge s (Lean.IndexedMinPQ.Op.insert v k) + C.potential (WordRAM.Data.comap f x)

Inline execution of P.callInsert: inserts (v, k) and charges 5 + C.charge s (.insert v k).

theorem Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callDecreaseKey_exec {B : WordRAM.Basis} {r_pq r_caller : ℕ} {P : PQCode B r_pq} {n K_max w base : ℕ} (C : WordRAM.SubroutineDS P.toSubroutineCode (Lean.IndexedMinPQ.spec n K_max) w base ![n] (Lean.IndexedMinPQ.empty n)) (hsp : n + 1 ≤ C.space) (hS : WordRAM.Fits w (base + C.space)) (hK : WordRAM.Fits w K_max) (harg_eq : C.argMatch = P.argMatch) {f : Fin r_pq → Fin r_caller} (hf : Function.Injective f) {zeroReg_c oneReg_c vReg_c kReg_c : Fin r_caller} (ho_out : oneReg_c ∉ Set.range f) (hv_out : vReg_c ∉ Set.range f) (hk_out : kReg_c ∉ Set.range f) {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data r_caller} {v : Fin n} {k : ℕ} (hr : C.rep s (WordRAM.Data.comap f x)) (hval : (∃ (k₀ : ℕ), s v = some k₀ ∧ k ≤ k₀) ∧ k ≤ K_max) (hz0 : x.regs zeroReg_c = 0) (ho1 : x.regs oneReg_c = 1) (hvv : x.regs vReg_c = ↑v) (hvk : x.regs kReg_c = k) : ∃ (z : WordRAM.Data r_caller) (t : ℕ), WordRAM.ExecWithin w (P.callDecreaseKey f zeroReg_c oneReg_c vReg_c kReg_c) x z t ∧ C.rep (Function.update s v (some k)) (WordRAM.Data.comap f z) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem z.mem ∧ (∀ j ∉ Set.range f, z.regs j = x.regs j) ∧ t + C.potential (WordRAM.Data.comap f z) ≤ 5 + C.charge s (Lean.IndexedMinPQ.Op.decreaseKey v k) + C.potential (WordRAM.Data.comap f x)

Inline execution of P.callDecreaseKey: lowers v's key to k and charges 5 + C.charge s (.decreaseKey v k).

theorem Cslib.Algorithms.WordRAM.PriorityQueue.PQCode.callGetKey_exec {B : WordRAM.Basis} {r_pq r_caller : ℕ} {P : PQCode B r_pq} {n K_max w base : ℕ} (C : WordRAM.SubroutineDS P.toSubroutineCode (Lean.IndexedMinPQ.spec n K_max) w base ![n] (Lean.IndexedMinPQ.empty n)) (hsp : n + 1 ≤ C.space) (hS : WordRAM.Fits w (base + C.space)) (harg_eq : C.argMatch = P.argMatch) (hdec_eq : C.decode = P.decode) {f : Fin r_pq → Fin r_caller} (hf : Function.Injective f) {zeroReg_c oneReg_c vReg_c : Fin r_caller} (hz_out : zeroReg_c ∉ Set.range f) (ho_out : oneReg_c ∉ Set.range f) (hv_out : vReg_c ∉ Set.range f) {s : Lean.IndexedMinPQ.State n} {x : WordRAM.Data r_caller} (v : Fin n) (hr : C.rep s (WordRAM.Data.comap f x)) (hz0 : x.regs zeroReg_c = 0) (ho1 : x.regs oneReg_c = 1) (hvv : x.regs vReg_c = ↑v) : ∃ (z : WordRAM.Data r_caller) (t : ℕ), WordRAM.ExecWithin w (P.callGetKey f zeroReg_c oneReg_c vReg_c) x z t ∧ P.decode (Lean.IndexedMinPQ.Op.getKey v) (WordRAM.Data.comap f z).regs = some (s v) ∧ C.rep s (WordRAM.Data.comap f z) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem z.mem ∧ (∀ j ∉ Set.range f, z.regs j = x.regs j) ∧ t + C.potential (WordRAM.Data.comap f z) ≤ 4 + C.charge s (Lean.IndexedMinPQ.Op.getKey v) + C.potential (WordRAM.Data.comap f x)

Inline execution of P.callGetKey: queries s v and charges 4 + C.charge s (.getKey v).

PQPackage: Parametric priority-queue implementation bundle

structure Cslib.Algorithms.WordRAM.PriorityQueue.PQPackage (B : WordRAM.Basis) (r_pq : ℕ) : Type

A priority-queue implementation over basis B with uniform PQCode B r_pq, memory footprint space n, per-operation amortized instruction charges *Time n, and parametric SubroutineDS certificates supporting arbitrary concrete potentials potential : Data r_pq → ℕ.

• code : PQCode B r_pq

  Uniform priority-queue code and register convention.

• space : ℕ → ℕ

  Memory footprint size on n handles ([base, base + space n)).

• space_lower (n : ℕ) : n + 1 ≤ self.space n

  Every priority queue on n handles reserves at least n + 1 words (n + 1 ≤ space n), so handle arguments v < n fit in w bits via Fits w (base + space n) in PQCode.arguments_fit.

• initTime : ℕ → ℕ

  Fresh-initialization instruction bound (initFresh).

• emptyTime : ℕ → ℕ

  Amortized instruction bound for isEmpty.

• getTime : ℕ → ℕ

  Amortized instruction bound for getKey.

• insertTime : ℕ → ℕ

  Amortized instruction bound for insert.

• decreaseTime : ℕ → ℕ

  Amortized instruction bound for decreaseKey.

• extractTime : ℕ → ℕ

  Amortized instruction bound for extractMin.

• cert {n K_max w base : ℕ} : WordRAM.Fits w (base + self.space n) → WordRAM.Fits w K_max → WordRAM.SubroutineDS self.code.toSubroutineCode (Lean.IndexedMinPQ.spec n K_max) w base ![n] (Lean.IndexedMinPQ.empty n)

  Parametric SubroutineDS certificate whenever base + space n and K_max fit in w bits.

• cert_space {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) : (self.cert hS hK).space = self.space n

  Certificate footprint agrees with space n.

• cert_initTime {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) : (self.cert hS hK).initTime ≤ self.initTime n

  Fresh initialization runs within initTime n instructions.

• cert_initPotential {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) : (self.cert hS hK).initPotential = 0

  Empty priority queue starts with initPotential = 0.

• cert_argMatch {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) : (self.cert hS hK).argMatch = self.code.argMatch

  Certificate argMatch agrees with code.argMatch.

• cert_decode {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) : (self.cert hS hK).decode = self.code.decode

  Certificate decode agrees with code.decode.

• charge_isEmpty {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) (s : Lean.IndexedMinPQ.State n) : (self.cert hS hK).charge s Lean.IndexedMinPQ.Op.isEmpty ≤ self.emptyTime n

  Amortized charge bound for isEmpty.

• charge_getKey {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) (s : Lean.IndexedMinPQ.State n) (v : Fin n) : (self.cert hS hK).charge s (Lean.IndexedMinPQ.Op.getKey v) ≤ self.getTime n

  Amortized charge bound for getKey.

• charge_insert {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) (s : Lean.IndexedMinPQ.State n) (v : Fin n) (k : ℕ) : (self.cert hS hK).charge s (Lean.IndexedMinPQ.Op.insert v k) ≤ self.insertTime n

  Amortized charge bound for insert.

• charge_decreaseKey {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) (s : Lean.IndexedMinPQ.State n) (v : Fin n) (k : ℕ) : (self.cert hS hK).charge s (Lean.IndexedMinPQ.Op.decreaseKey v k) ≤ self.decreaseTime n

  Amortized charge bound for decreaseKey.

• charge_extractMin {n K_max w base : ℕ} (hS : WordRAM.Fits w (base + self.space n)) (hK : WordRAM.Fits w K_max) (s : Lean.IndexedMinPQ.State n) : (self.cert hS hK).charge s Lean.IndexedMinPQ.Op.extractMin ≤ self.extractTime n

  Amortized charge bound for extractMin.

def Cslib.Algorithms.WordRAM.PriorityQueue.PQPackage.mapSimulates {B B' : WordRAM.Basis} {r_pq : ℕ} (φ : B.Simulates B') (pkg : PQPackage B r_pq) : PQPackage B' r_pq

Translate a PQPackage along any basis simulation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.PriorityQueue.PQPackage.toStandard {r_pq : ℕ} (pkg : PQPackage WordRAM.Basis.exact r_pq) : PQPackage WordRAM.Basis.standard r_pq

Lift an exact-basis PQPackage to Basis.standard.