docs: coinage management component design#122
Draft
TorstenStueber wants to merge 184 commits into
Draft
Conversation
Two new design docs under docs/design/ specifying the host's internal coinage subsystem and its API contract. Sufficient to implement RFC-6 and RFC-17 on top. - coinage-management.md: design and rationale (concepts, data model, operational model, operation lifecycle, security, recovery, tunable parameter recommendations). - coinage-management-contract.md: detailed records, state machines, subscriptions, operation primitives, receipts, errors, events.
Bottom-layer (Coinage Layer) of the two-layer coinage subsystem, split out from the prior unified coinage-management design. Companion Quint specification models the full state machine — purses, coins, recycler entries, operations, rings, receipts, events, unload tokens, fee account, anonymity floor — and asserts 24 safety invariants covering value conservation, lock consistency, derivation determinism, the ring-rescue contract, and anonymity-floor enforcement. Also adds work notes capturing the design decisions, the iOS silent-loss-of-funds bug the spec encodes against, and the path to behavioral conformance verification against a real implementation.
…o add-coinage-design
…i-group unload, gap-limit recovery Expands the bottom-layer Quint spec from ~3066 to 3726 lines, raising design-document coverage from ~85% to ~92-93%. Three new design areas are now operational rather than predicate-only: 1. Deterministic multi-coin selection (§6.3 tier 1) — `selectExactCoverDeterministic` returns the unique lex-min exact cover under the priority ordering; `startTransferDeterministicMulti` locks the deterministic subset. 2. Multi-group unload (§8.6) — `startExternalOffloadMulti` locks a set of entries; `opOffboardGroup` submits one extrinsic per (denomination, ring) group with per-group surplus reload; `opCompleteExternalOffload` asserts externalized total equals requested. Legacy single-entry `opOffboard` gated to one locked entry. 3. Gap-limit recovery (Appendix C) — `chainCoins`/`chainEntries` mirror chain-side storage; pure `gapLimitScanCoins`/`gapLimitScanEntries` implement the batched scan; `restartAndRecover` atomic loss+recovery; `recover` refactored to gap-limit semantics with cursor advancement. Other changes: - 28-invariant `safety` aggregate, all individually clean on simulator. - `anonymityFloorEnforced` moved out of `safety` — `deletePurse` shrinks rings post-seal; floor is a per-promotion property already enforced by `chainPromoteToReady`'s precondition. - New invariant `chainMirrorsLocal` — every local record present in chain. - Updated work-notes capture the path forward to Verus implementation.
Adds a new workspace crate `coinage-layer` translating the purse-lifecycle portion of the Quint spec into Verus-verified Rust. Pilot scope: `init`, `create_purse`, `query_purse`. State is restricted to the `purses` map plus a fresh-id allocator; coins, entries, operations, events, and tokens are out of scope and will follow in subsequent commits. Encoding: exec storage is a `Vec<PurseRec>`; contracts quantify over a ghost `Map<PurseId, PurseRecSpec>` mirror. The refinement invariant ties them: every Vec entry is in the ghost map under its own id, every map key has a Vec witness, and no duplicate ids exist in the Vec. This is what lets `query_purse`'s linear scan satisfy a contract phrased against the ghost map. `cargo verus verify` reports 5 verified, 0 errors. `cargo build --workspace` stays clean. Divergence noted: Quint's `createPurse(newId, nm)` takes the id as a caller-supplied parameter; the design has the layer allocate. The Rust follows the design — the allocator (`next_purse_id`) discharges the Quint freshness precondition by construction.
…rity invariant
Extends the Verus pilot with three operations and one invariant addition:
* `rename_purse(p, name)`: in-place Vec index-mut, ghost-map insert.
Strong contract: dom unchanged; name and other fields updated
field-by-field; off-target entries unchanged.
* `delete_purse(p)`: rejects MAIN_PURSE; uses `Vec::swap_remove` plus
`Map::remove`. Strong contract: result is `old.purses().remove(p)`
in the Ok branch; state unchanged in either error branch.
* Coin state (ghost-only for now): `spec_coins: Ghost<Map<(PurseId, u64),
CoinRec>>` and a `CoinRec` type. Invariant gains two clauses — key
consistency (`coin.purse == key.0`, `coin.idx == key.1`) and
referential integrity (`coin.purse` must be in `purses().dom()`).
`delete_purse` therefore gains a precondition forbidding deletion
while any coin still references the purse.
The exec field `spec_purses` was made `pub` so the `open spec fn`
accessors (`purses()`, `coins()`, `has_coin_in()`, `invariant()`) can
inline at call sites outside this crate; Verus treats a struct with even
one private field as fully opaque externally.
`cargo verus verify` reports 9 verified, 0 errors. Workspace build is
clean.
Adds the elemental coin-creation operation to the Verus pilot:
* Invariant clause (k): `coin.idx < purses[coin.purse].next_coin_idx`.
Consequence: the purse's `next_coin_idx` is always a fresh coin idx
for that purse, so `add_coin` needs no separate freshness check.
* `add_coin(p, exponent)`: locates `p` in the exec Vec, bumps the
purse's `next_coin_idx` field via `IndexMut`, inserts a `CoinRec`
into the ghost coin map at key `(p, old_next_coin_idx)`. Strong
contract: returns the assigned key; the purse record keeps id,
name, and next_entry_idx; only next_coin_idx advances by one; off-
target purses unchanged; coins map gains exactly the new entry.
Existing operations (init, create_purse, rename_purse, delete_purse,
query_purse) continue to verify under the strengthened invariant —
trivially, since they do not touch coins.
`cargo verus verify`: 11 verified, 0 errors. Workspace build clean.
Adds the first composite operation and the coin lifecycle, exercising
both the ability to call `add_coin` in a verified loop and the ability
to evolve coin records through ghost-state transitions.
* `top_up_purse(p, exp_seq)`: loops `add_coin` for each exponent in
`exp_seq`. Strong contract: purse `p` exists, dom unchanged, p's
`next_coin_idx` advances by exactly `exp_seq.len()`, every old
coin is preserved, and for each `j` the new key `(p, old_next + j)`
is in the coin map with `exponent == exp_seq[j]`. Loop-invariant
pattern: capture `pre_coins` before each `add_coin` call and use
`dom().contains(...)` as the quantifier trigger (rather than
`exp_seq@[j]`, which was too weak).
* `CoinState` enum (`Available`, `PendingSpend`, `Spent`) added to
`CoinRec`; `add_coin` now creates coins as `Available`.
* `mark_coin_pending_spend` / `mark_coin_spent`: state transitions
`Available → PendingSpend → Spent`. Ghost-only at the exec level
in this pilot; will mutate the actual record once exec coin
storage lands.
* `has_live_coin_in(p)`: predicate for "any non-Spent coin in p".
* `delete_purse` precondition relaxed from "no coin in p" to "no
live coin in p", and the body now filters spec_coins to drop all
keys with first component p. Postcondition extended to express the
coin-map removal: `final.coins() == old.coins().remove_keys({k:
k.0 == p})`.
`cargo verus verify`: 15 verified, 0 errors. Workspace build clean.
Updates `COINAGE-LAYER-WORK-NOTES.md` §11-13 to reflect the actual state of the Verus pilot landed across commits 1289ee2..b86141c: 9 verified operations, 11 invariant clauses (a-k), 15 verified / 0 errors. Adds an explicit "Pilot scope honesty" subsection documenting what is *not* implemented (exec coin storage, real spendable, value semantics, ages, accounts, entries, unload tokens, operations, chain mirror) and why the exec coin Vec extension was queued as stage 5 work — the delete_purse filter-rebuild proof was beyond the pilot's time-box. Adds `VERUS-BY-EXAMPLE.md` capturing the 14 proof-engineering patterns that crystallized during the pilot: state struct shape, view() lift, pre-state ghost capture trio, trigger choice rule, loop invariant template, per-clause assert-forall blocks, captured-before-move idiom, compositional looping, `old()` / `final()` syntax, `unreached()` for invariant-derived dead code, workspace build hygiene, proof economy ratio (~6:1), and decomposition rule for runaway proofs. The goal is that the next operation translated from the Quint spec to Verus reuses these patterns without re-discovering them.
Adds a real `Vec<CoinRec>` exec field alongside the ghost coin map, with
three new invariant clauses tying them:
(l) every Vec entry's `(purse, idx)` is in `spec_coins.dom()` and the
ghost record matches.
(m) every ghost-dom key has a Vec witness.
(n) no duplicate `(purse, idx)` keys in the Vec.
CoinRec and CoinState are now `Copy` + `Clone` (lets a filter-rebuild
loop read entries without ownership friction in later stages).
Operations updated:
* `init` initializes `coins` to an empty Vec.
* `add_coin` now pushes the constructed `CoinRec` into `self.coins`
and proves (l, m, n) post-push. The key fact for (n) is that the
new key `(p, cur_idx)` cannot collide with any pre-existing entry,
because invariant (k) bounds every old coin's `idx` strictly below
`purses[purse].next_coin_idx`, which equals `cur_idx` for `purse == p`.
* Both `mark_coin_*` now delegate to a private helper
`transition_coin_state(key, new_state)` that scans the Vec for the
target entry, mutates its `state` field via `IndexMut`, and mirrors
to the ghost map. Helper's proof block re-establishes (a-n) using
the per-clause `assert forall ... by { ... }` pattern.
* `delete_purse` has its precondition temporarily tightened to forbid
any coin in `p` (stage 5e will reintroduce a `purge_coins_of_purse`
call and relax it back to `!has_live_coin_in`).
`cargo verus verify` reports 19 verified, 0 errors. Workspace builds
clean.
Adds three coordinated operations: `find_coin_with_purse(p)` returns the first Vec index whose entry has `purse == p` (or `None`); `remove_coin_at(idx)` does one `swap_remove` plus matching ghost `remove`, with full per-clause proof of (a-n) preservation; `purge_coins_of_purse(p)` loops the two until no coin in `p` remains. The decomposition was the key. The earlier attempt (single inline filter-rebuild loop) blew past 200 proof lines; this split contains each proof to ~150 lines for `remove_coin_at` and ~50 for `purge`. `remove_coin_at`'s contract is a clean `coins() == old.coins().remove(k)` which the outer loop composes via a subset-preserving loop invariant. The post-loop "no coin with purse == p remains" fact is proven inside the `None` branch of the find call (where `forall j. coins[j].purse != p` is in scope), then combined with invariant (m) to conclude the final `remove_keys` equality via contradiction reasoning. `cargo verus verify` reports 24 verified, 0 errors.
`delete_purse` now calls `purge_coins_of_purse(p)` at the top, then
proceeds with the existing scan-and-remove of the purse record. The
precondition relaxes from "no coin in p at all" (stage 5a tightening)
back to `!has_live_coin_in(p)` — Spent coins in p are tolerated and
get purged in the body. The postcondition now exposes the coin-map
change explicitly: `final.coins() == old.coins().remove_keys({k: k.0
== p})` in both the Ok branch and the PurseNotFound branch (where it
reduces to the identity because invariant (j) implies no coin had
purse == p anyway).
Composition pattern: `purge_coins_of_purse` and `remove_coin_at` both
gained explicit clauses on the purse Vec and `next_purse_id` being
unchanged. Without these, the post-call state was insufficient to
re-establish the existing purse-removal loop invariant.
Pilot status: 24 verified, 0 errors. The full lifecycle now exists in
exec form: init → create_purse → top_up_purse (loops add_coin) →
mark_coin_pending_spend → mark_coin_spent → purge_coins_of_purse →
delete_purse. The remaining stage-5 deliverables — `query_purse.spendable`
via Vec scan, coin-selection primitive — are now mechanically reachable.
Adds a free spec function `count_avail_prefix(v, p, j)` defined recursively over a `Seq<CoinRec>` prefix, returning the count of Available coins in purse `p` among `v[0..j]`. This is the contract surface for spendable. `count_available_in(p)`: exec scan of `self.coins` returning `u64`, loop-invariant tied to `count_avail_prefix`. The non-trivial proof ingredient is a single inline `assert` that `count_avail_prefix(v, p, j+1) <= count_avail_prefix(v, p, j) + 1` — used both to discharge the no-overflow check on `count + 1` and to maintain the `count <= j` invariant that prevents the count from overshooting Vec length. `query_purse`: spendable is now real — `i.spendable as nat == count_avail_prefix(self.coins@, p, len)`. `spendable_strict` and `pending` remain pilot-stubbed at 0 (those depend on recycler-entry state which is out of pilot scope). **Pilot value scheme caveat:** spendable counts Available coins, it does not sum coin values. Real `coinValue(exp) = 2^exp` is deferred. The contract uses cardinality semantics, which is well-defined and verifiable; switching to sum-of-values would require additional overflow / nonlinear reasoning. `cargo verus verify` reports 27 verified, 0 errors.
Adds `select_coin(p, min_exponent) -> Option<(PurseId, u64)>` which scans the coin Vec for the first `Available` coin in purse `p` whose `exponent >= min_exponent`. Strong contract: Some(key) ⇒ key in coins.dom + state Available + exponent ≥ threshold. None ⇒ no coin in p is Available at that threshold. The None branch's proof uses invariant (m) to lift the Vec-scan "not-found" fact to a universal statement over the ghost map: any ghost key with the wrong properties has a Vec witness with matching fields (by (l)), contradicting the loop's accumulated negation. This is the last primitive needed before composite operations (`transfer`, `rebalance`) can be modeled — they all decompose into `select_coin` + `mark_coin_pending_spend` + chain-side commit + `mark_coin_spent`. `cargo verus verify` reports 29 verified, 0 errors. Workspace builds clean.
Adds `transfer(from, to, min_exp) -> Option<(PurseId, u64)>` exercising
the full composition pattern that the pilot has been building toward:
1. `select_coin(from, min_exp)` → either no candidate or some key.
2. `read_coin_exponent(key)` → captured BEFORE marks (the marks don't
touch the exponent field but reading after them would require
extra proof to chain through the ghost-record equality).
3. `mark_coin_pending_spend(key)` — Available → PendingSpend.
4. `mark_coin_spent(key)` — PendingSpend → Spent. Together these
simulate chain settlement of the spend.
5. `add_coin(to, exp)` — mint the destination coin with the same
exponent.
Strong contract: Some result is a fresh Available coin in `to` with
exponent ≥ min_exp; None means no Available coin in `from` met the
threshold.
Verified in ~10 lines of exec code with NO proof block. Each step's
postcondition automatically discharges the next step's precondition.
That is the whole point of the contracts work — once the primitives
have strong contracts, composition is essentially mechanical.
Also adds `read_coin_exponent(key)` helper (small Vec scan with the
standard "unreachable via invariant (m)" tail).
`cargo verus verify` reports 32 verified, 0 errors.
`COINAGE-LAYER-WORK-NOTES.md` §12-13 rewritten to reflect the 32-verified
state with all eleven commits enumerated and the composite `transfer`
operation listed. "Pilot scope honesty" trimmed: exec coin storage, real
spendable, and coin-selection primitive are now done; remaining deferred
work is value semantics, recycler entries, operations/chain, ages,
accounts.
`VERUS-BY-EXAMPLE.md` gets four new sections (§14-18):
§14 — decomposition rule (with the delete_purse/purge worked example)
§15 — sibling-field stability is part of the contract, not just the body
§16 — composition pattern that lets composite ops verify with zero
proof blocks (worked through `transfer`)
§17 — recursive spec functions for aggregations (`count_avail_prefix`,
overflow-bound proof via inline assert)
§18 — `matches!` workaround for enum equality in exec code
Proof economy section updated with actuals: 250 exec / 280 spec / 1,600
proof for primitives, ZERO proof for composite operations.
Adds `rebalance(src, dst, key)` mirroring Quint §6.1.3 rebalancePurse. Unlike `transfer`, the caller selects the specific coin by key (no min-exp search); the body composes `read_coin_exponent` → marks → `add_coin` exactly as `transfer` does. Contract is stronger than transfer's because the input key is known: the postcondition pins down both the source coin's final state (Spent) and the new coin's (dst, old_dst_next_coin_idx) position with matching exponent. Verified in 5 exec lines with no proof block. Same payoff as transfer: strong primitive contracts mean composite operations cost nothing to verify. `cargo verus verify` reports 33 verified, 0 errors.
Adds the entry-side state surface without yet exposing operations:
* `EntryOnChain` enum (Missing/Waiting/Ready/Degraded) — Quint
EntryOnChain, minus the post-submission detection epoch payload.
* `EntryRec { purse, idx, exponent, on_chain }` — pilot subset of
Quint EntryRec (memberKey, allocatedAt, readyAt, ringIdx, and
EntryLocal deferred).
* `entries: Vec<EntryRec>` exec field and `spec_entries: Ghost<Map<...>>`
ghost field on State, with parallel structure to coins.
* Six new invariant clauses (o-t):
(o) entry key consistency
(p) entry referential integrity to purses
(q) entry idx below the owning purse's `next_entry_idx`
(r,s) Vec ↔ ghost refinement
(t) no duplicate (purse, idx) entry keys
* `entries()` spec accessor.
Existing operations are updated to maintain the new clauses (they all
hold trivially because entries is empty in the pilot and never mutated
in this commit). `delete_purse` gets a temporary precondition
forbidding any entry in p; this is relaxed in stage 6c once
`purge_entries_of_purse` lands.
`purge_coins_of_purse` and `remove_coin_at` gain explicit
`final.entries@ == old.entries@` and `final.spec_entries@ == old.spec_entries@`
clauses — the sibling-field stability pattern again (VERUS-BY-EXAMPLE §15).
Without these, delete_purse can't carry entries across the purge call.
`cargo verus verify` reports 35 verified, 0 errors.
Adds `add_entry(p, exponent, on_chain)` mirroring `add_coin`'s
structure for the entries side. Allocates `(p, next_entry_idx)`,
pushes the new EntryRec to both the exec Vec and the ghost map,
bumps the purse's `next_entry_idx`.
Contract:
* `key.1 == old.purses[p].next_entry_idx` (allocator-determined)
* `final.entries() == old.entries().insert(key, EntryRec { ... })`
* `final.coins() == old.coins()` (coins untouched)
* `final.purses[p].next_coin_idx` unchanged
* `final.purses[p].next_entry_idx == old + 1`
Proof structure is a direct mirror of `add_coin`'s ~150-line block:
purse-side (a-h), coin-side (i, j, k) carried through unchanged, and
the new entry-side (o, p, q, r, s, t) re-established post-push. The
key fact for (t) is that the new key (p, cur_idx) cannot collide
because invariant (q) bounds every old entry's idx strictly below
old_m[entry.purse].next_entry_idx == cur_idx (for purse == p).
`cargo verus verify` reports 37 verified, 0 errors.
…ge 6c)
Adds three coordinated entry-side operations mirroring the coin
purge stack:
* `find_entry_with_purse(p)` — first Vec index whose entry has
purse == p, else None.
* `remove_entry_at(idx)` — swap_remove + ghost remove on entries,
with full per-clause proof of (a-t) preservation (entries-side
clauses (o-t) get the heavy work; coin-side (i-n) and purse-side
(a-h) follow unchanged).
* `purge_entries_of_purse(p)` — loops the two until no entry in p.
Postcondition matches purge_coins_of_purse: spec map is
`old.entries().remove_keys({k.0 == p})`.
`delete_purse` now composes both purges:
```
self.purge_coins_of_purse(p);
self.purge_entries_of_purse(p);
// then existing purse-removal scan
```
Precondition relaxes: only `!has_live_coin_in(p)` is required at the
caller level. Spent coins and entries in any state are purged
automatically. PurseNotFound branch's contract correctly reflects
that coins and entries get filtered by `remove_keys({k.0 == p})`,
which is the identity when no coin/entry has purse == p (guaranteed
by invariants (j)/(p)).
The decomposition into find / remove_at / purge has now proven
itself twice — same shape worked unchanged for both coins and
entries, ~250 proof lines each. Mechanical pattern.
`cargo verus verify` reports 42 verified, 0 errors.
Adds the entry-side state transition primitive `set_entry_on_chain(key, new_state)`. Mirrors `transition_coin_state`'s structure: scan the entry Vec for the target key, mutate its `on_chain` field via IndexMut, mirror to the ghost map, prove (a-t) preserved. Generalized — any transition between EntryOnChain states (Missing → Waiting → Ready → Degraded etc.) is accepted; valid transition orderings are a layer-above concern (Quint's `chainPromoteToReady` etc. set the specific state transitions). Recycler entries are now structurally on par with coins: full Vec ↔ ghost refinement, allocation (`add_entry`), purge (`purge_entries_of_purse` via find/remove_at decomposition), state transition (`set_entry_on_chain`), and integration with delete_purse. The proof is the seventh near-identical mirror of the pattern from VERUS-BY-EXAMPLE §7 (per-clause assert-forall blocks for one-field Vec mutation). At this point the proof is mechanical: change the type, change the field, change the names — clauses (a-t) re-discharge. `cargo verus verify` reports 44 verified, 0 errors. Workspace builds clean.
Extends the coin lifecycle to four states matching design §5.1: Pending → Available → PendingSpend → Spent. New `add_coin` allocates in Pending (faithful to design: newly-allocated coins must be observed on chain before becoming spendable). `mark_coin_observed(key)`: Pending → Available transition. Thin wrapper around the existing `transition_coin_state` helper. Composite operations `transfer` and `rebalance` call mark_coin_observed internally on their destination coins, so their contracts (which promise destination state == Available) remain unchanged. `top_up_purse` leaves new coins in Pending state — the caller observes them when appropriate. Verus discharged with no proof changes beyond the new mark wrapper: the established lifecycle pattern (transition_coin_state) already handles arbitrary CoinState values. `cargo verus verify` reports 45 verified, 0 errors.
Adds the entry-local lifecycle state from design §5.4: LocalAvailable / LocalLockedFor / LocalConsumed. The LockedFor variant drops its operation-handle payload (no ops subsystem yet). `EntryRec` gains a `local` field. `add_entry` signature extends to take the initial local state. `set_entry_local(key, new_state)` is a parallel of `set_entry_on_chain` for the `local` field — same ~180- line proof structure, mechanical mirror. The pattern continues to scale: ninth and tenth uses of the per-clause assert-forall block. Cost per state-field-mutating primitive remains ~120 proof lines for the active branch + ~50 boilerplate for the ghost capture quad and find-then-return tail. `cargo verus verify` reports 48 verified, 0 errors.
Replaces the previous count-based spendable with a value-based sum:
* New spec function `coin_value(exp: u8) -> nat = (exp as nat) + 1`.
Pilot scheme — linear and monotone in exp, captures "bigger exp
means bigger value" without overflow gymnastics. Real `2^exp` is
deferred until saturating-arithmetic specs are in place.
* `count_avail_prefix` → `sum_avail_prefix`. Body sums `coin_value(exp)`
over Available coins instead of incrementing by 1.
* `count_available_in` → `sum_available_in`. Loop invariant pinned
via `assert(sum_avail_prefix(_, p, j+1) <= sum_avail_prefix(_, p, j) + 256)`
— the per-step delta is bounded by `coin_value(_) <= 256`. The
cumulative `u64` sum is kept safe by a precondition `coins.len() <=
u64::MAX / 256` (caller's responsibility).
* `query_purse.spendable` now reports the value sum.
`cargo verus verify` reports 48 verified, 0 errors. Workspace builds clean.
The pilot value scheme is honest about its limitation: real `2^exp`
will need either saturating arithmetic or a bound on simultaneous
high-exponent coins. Both are doable but out of scope for this
mechanical-extension stage.
Lands all 17 error variants from design §10:
Pre-submission: PurseNotFound, OperationNotFound, CannotDeleteMainPurse,
PurseHasInFlightOperations, OutputsDoNotSumToAmount, InsufficientFunds,
InsufficientExternalFunds, NoReadyEntries, NoUnloadToken, BadCoinSecret.
Post-submission: SnipedCoin, ChainRejected.
Lifecycle: Cancelled, InterruptedPreSubmission.
Internal: StorageError, SubscriptionError, RecoveryFailed, Internal.
Verus-compat stubs:
* `String` → `Vec<u8>` (Verus models String via Seq<char>, but Vec<u8>
works for opaque error payloads without spec gymnastics).
* `OperationHandle` → `u64` placeholder (no ops subsystem yet).
* `ExtrinsicHash` → `u64` placeholder (no chain interaction).
Existing match arms in rename_purse, delete_purse, query_purse contracts
now use `Err(_) => false` catch-alls — the functions never return any of
the new variants in the current scope, but the type-level exhaustiveness
no longer forces variant-by-variant enumeration.
`cargo verus verify` reports 48 verified, 0 errors.
Adds `select_coins_for_amount(p, requested) -> Option<Vec<(PurseId, u64)>>`
exercising multi-coin reasoning. Scans Available coins in Vec order,
accumulates value, returns the selected keys once `sum >= requested`.
None when total Available value in p falls short of `requested`.
Contract:
Some(keys): every key is an Available coin in p, and the sum of their
coin_values meets or exceeds requested.
None: sum_avail_prefix(_, p, len) < requested. (No subset of
Available coins could have satisfied the request.)
New spec `sum_of_coin_values(coins, keys: Seq<...>)` defined recursively
on the key sequence, lifts to the contract surface.
The loop-invariant pair
accumulated == sum_avail_prefix(self.coins@, p, j as nat)
accumulated == sum_of_coin_values(self.coins(), selected@)
ties the scan-cumulative to both the prefix-sum view (used in the None
branch) and the selected-keys view (used in the Some branch). Both are
maintained by the same single assertion that pushing a key adds its
coin_value to sum_of_coin_values (subrange decomposition).
**Pilot scope:** this is NOT the design's three-tier exact-cover
selection (§6.3). Greedy may overshoot. Exact subset-sum is documented
as deferred — needs powerset enumeration with lex-min disambiguation
(Quint `selectExactCoverDeterministic`).
Preconditions:
* `coins.len() <= u64::MAX / 256` — keeps cumulative sum in u64.
* `requested <= u64::MAX - 256` — keeps `accumulated + value` safe.
* `requested >= 1` — empty selection trivially "covers" 0.
`cargo verus verify` reports 51 verified, 0 errors.
Adds `split_coin(key, new_exponents)` modeling design §6.3 Tier-2 split. Composes existing primitives: mark_coin_pending_spend(key) // Available → PendingSpend mark_coin_spent(key) // PendingSpend → Spent top_up_purse(key.0, new_exps) // allocates one new Pending coin per exp Source coin terminates; new coins occupy sequential next_coin_idx slots in the same purse. Strong contract pins down the source coin's terminal state and the position+exponent of each new coin. The body is 5 exec lines + one 2-line proof hint (the post-`mark_spent` coin map is captured before the `top_up_purse` call so Verus carries the source coin's state through into the final state). Cleaner demonstration of contract chaining than `transfer`, since `top_up_purse` itself is already a loop-based composite. **Pilot scope:** no value-preservation check between source exponent and sum of new exponents. Real splits require `coin_value(source) == sum(coin_value(new_i))`; deferred until real 2^exp semantics (see stage 7c). `cargo verus verify` reports 52 verified, 0 errors.
…k_op_waiting + strengthen and refine release_entry_lock
…omposed over with_account/with_meta)
…entry (some/none)
…none, composed via release_locked)
…urse_safe (success/main/notfound)
…th existential src_key
…with-witness/none)
…lit_coin (bulk-loop composites)
|
Review the following changes in direct dependencies. Learn more about Socket for GitHub.
|
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
Two new design docs under
docs/design/specifying the host's internal coinage subsystem and the contract above it. Together they are sufficient to implement RFC-6 and RFC-17 without ambiguity. Written abstractly — no reference to existing implementations.coinage-management.md— design and rationale. Architecture, core concepts (purse, coin, recycler entry, receivable, cheque, operation), data model (states, lifecycles, derivation), operational model (observation, balance, selection, recycling, unload tokens, fees), operation lifecycle, security boundaries, recovery, tunable parameter recommendations.coinage-management-contract.md— detailed API contract. Durable records, state machines, subscription primitives, operation primitives, receipts, error taxonomy, event taxonomy, recommended derivation scheme, recommended recovery algorithm.