RFC: Route Relay#92
Open
pgherveou wants to merge 3 commits into
Open
Conversation
Proposes host_route_get / host_route_set / host_route_changed so apps running in a Web host can publish their internal route to the address bar, restore deep-linked state at bootstrap, and react to Host back/forward without accessing the URL bar directly.
Wire IDs 134, 136 (unary) and 138 (stream) on the System trait. Adds the v0.1 types, versioned envelopes, and trait methods. Also documents the Web-host shim where these methods can be reached transparently via the standard history.pushState / popstate API.
Splits the route surface and external-URL open out of System into a dedicated Navigation trait. Wire IDs are unchanged (6 for navigate_to, 134/136/138 for route_get/route_set/route_changed); only the trait membership and the v0.1 / versioned module layout move.
Contributor
|
I think this logic should be simplified to a single
|
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 nextExtrinsicId counter on State:
State.next_extrinsic_id: u64
alloc_extrinsic_id() -> u64 bumps counter; returns previous
read_next_extrinsic_id() -> u64 pure read
Second confirmation that the State-extension cascade pattern is
template-able. Fields fee_balance and next_extrinsic_id together
demonstrate the playbook:
1. Add State field + init zero.
2. replace_all `final.X == old.X` after every `final.next_age == old.next_age`.
3. replace_all the same for loop invariants.
4. For mutators that change X, use the ghost-capture scaffold from
[[feedback-verus-ghost-field-mutation]] to assert siblings unchanged.
Each step took seconds. Pattern unlocks unload tokens (#89) and is
the same shape needed for events Vec (#92) — just with Seq<Event>
in place of u64.
216 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
3 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
Proposes a small host-API surface that lets an embedded app participate in the Host's address bar:
host_route_get— read the current route (used at bootstrap to restore deep-linked state)host_route_set— publish the app's current route (push or replace), so it appears in the Host URL and survives reload / sharinghost_route_changed— stream of external route changes (Host back/forward, pasted URL)Routes are opaque to the Host; apps define their own format.
Motivation
Apps running in a Web host are loaded in a webview / iframe. The address bar belongs to the Host, so
history.pushState/ hash routing inside the iframe is invisible, unshareable, and lost on reload. There is currently no way to deep-link into a sub-route or react to Host-driven navigation.