Remove unused PaymentPurse alias and CoinPaymentInvoice type - #90
Merged
filvecchiato merged 1 commit intoMay 15, 2026
Merged
Conversation
- PaymentPurse is defined but never referenced - CoinPaymentInvoice is a product-constructed wire format not used by any host trait method; the RFC documents it as a spec
pgherveou
approved these changes
May 15, 2026
filvecchiato
merged commit May 15, 2026
0e97fd3
into
codex/rfc-0016-merchant-payments
9 checks passed
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
Adds the fee_balance field to State + four typed ops:
State.fee_balance: u64 (Quint feeAccountBalance)
FeeMode { Prepaid, FromOutput } (Quint FeeMode)
top_up_fee_account(amount) -> () (Quint topUpFeeAccount)
deduct_fee(amount) -> Result<(), Error>
read_fee_balance() -> u64
select_fee_mode(fee) -> FeeMode
The cascade landed via two-pass approach:
Pass 1 (mechanical): replace_all adds
`final(self).fee_balance == old(self).fee_balance` after every
existing `final(self).next_age == old(self).next_age` postcondition,
and the parallel form for every loop invariant. 42 + 10 sites
auto-updated; baseline stays at 209 verified.
Pass 2 (per-function): the two fee-account mutators that DO change
fee_balance need ghost-capture proof scaffolding so Verus can see
the partial-mutation preserves all other State fields. Same
pattern documented in [[feedback-verus-ghost-field-mutation]]:
capture old_*_vec / old_spec_* ghosts before the mutation, assert
equality afterwards.
Unlocks task #89 (unload tokens) and is a template for the larger
events Vec cascade (task #92).
214 verified, 0 errors.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
Adds the Quint event stream:
Event enum: 8 variants matching Quint Event types
(CoinAvailable, CoinSpent, EntryAllocated, EntryReadinessChanged,
EntryConsumed, OperationStarted, OperationProgress,
OperationCompleted)
State.events: Vec<Event>
emit_event(e) -> () append-only primitive
event_count() -> usize event-stream length
The cascade landed via the same two-pass playbook from #90:
1. Bulk add `final.events@ == old.events@` after every
`final.next_extrinsic_id == old.next_extrinsic_id` site
(postconditions + loop invariants).
2. New emitter functions use the ghost-capture scaffold.
The events field is the biggest possible State extension by surface
area, and it landed without any per-function chasing — proving the
playbook is robust. From here, every wrapper that should emit events
(tracked_transfer, mark_op_done, etc.) just needs to add an
emit_event call + declare the emission in its postcondition.
219 verified, 0 errors.
TorstenStueber
added a commit
that referenced
this pull request
May 26, 2026
…ssion
Adds the Quint unload-token mechanics (§6.5):
UnloadTokenClass { Free, Paid }
UnloadToken { period, class, counter, consumed }
State.tokens: Vec<UnloadToken>
mint_token(period, class, counter) -> usize chain emits token
consume_token(idx) -> Result<(), Error> flip consumed flag
token_count() -> usize reader
consume_token is idempotent: returns Err(Internal) if the index is
out of range OR the token is already consumed; state stays unchanged
in both cases. Future work: surface a typed UnloadTokenNotAvailable
error variant.
This completes all four State-extension items raised by the user's
"are we stuck on Phase 6?" question. The proven cascade pattern
landed every one:
- fee_balance (task #90 ✅)
- next_extrinsic_id (just-shipped)
- events (task #92 ✅)
- total_in / total_out / paid_ring_membership
- tokens (task #89 ✅)
229 verified, 0 errors. The cascade isn't a blocker anymore — it's
a standard template.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
PaymentPursetype alias fromv01/payment.rs— defined but never referencedCoinPaymentInvoicestruct fromv01/coin_payment.rs— product-constructed wire format not used by any host trait method (the RFC documents it as a spec)Test plan
cargo build --workspacecargo test --workspace— all 18 tests passcargo +nightly fmt --checkcargo clippy --workspace --all-targets --all-features -- -D warnings