From 1c08ed52a4a3bf16576c2f254a400d4df24cac12 Mon Sep 17 00:00:00 2001 From: Santiago Date: Fri, 21 Aug 2026 17:16:29 -0300 Subject: [PATCH 1/3] chore(experimental): add Quint de-risk spike for the Conway phase-1 UTXO slice Phase 0b of the phase-1 validation effort: a de-risk experiment measuring whether a Quint executable spec replayed via quint-connect can serve as the living spec and test oracle for the phase-1 rules. - spec/conway_utxo.qnt: Quint model of a Conway UTXO slice (fee floor, preservation of value, size bounds, collateral bounds) with per-rule trace generators - src/lib.rs: the same checks behind a caller-supplied UtxoContext boundary, with four mutate-* features seeding deliberate defects - tests/mbt.rs: quint-connect driver replaying model traces against the spike, full-state diff every step - EVIDENCE.md: modelability notes, rule coverage, mutation matrix, effort record and extrapolation The crate is its own workspace root: excluded from the pallas workspace, its CI, and its publish surface. It is experiment evidence, not the phase-1 implementation. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_013akZUCHm87no6x9Utvh8eP --- experimental/quint-derisk/.gitignore | 1 + experimental/quint-derisk/Cargo.toml | 25 ++ experimental/quint-derisk/EVIDENCE.md | 158 +++++++++ experimental/quint-derisk/README.md | 44 +++ experimental/quint-derisk/bin/quint | 3 + .../quint-derisk/spec/conway_utxo.qnt | 301 ++++++++++++++++++ experimental/quint-derisk/src/lib.rs | 284 +++++++++++++++++ experimental/quint-derisk/tests/mbt.rs | 219 +++++++++++++ 8 files changed, 1035 insertions(+) create mode 100644 experimental/quint-derisk/.gitignore create mode 100644 experimental/quint-derisk/Cargo.toml create mode 100644 experimental/quint-derisk/EVIDENCE.md create mode 100644 experimental/quint-derisk/README.md create mode 100755 experimental/quint-derisk/bin/quint create mode 100644 experimental/quint-derisk/spec/conway_utxo.qnt create mode 100644 experimental/quint-derisk/src/lib.rs create mode 100644 experimental/quint-derisk/tests/mbt.rs diff --git a/experimental/quint-derisk/.gitignore b/experimental/quint-derisk/.gitignore new file mode 100644 index 000000000..ea8c4bf7f --- /dev/null +++ b/experimental/quint-derisk/.gitignore @@ -0,0 +1 @@ +/target diff --git a/experimental/quint-derisk/Cargo.toml b/experimental/quint-derisk/Cargo.toml new file mode 100644 index 000000000..31ebedc0d --- /dev/null +++ b/experimental/quint-derisk/Cargo.toml @@ -0,0 +1,25 @@ +[package] +name = "conway-utxo-quint-spike" +version = "0.0.0" +edition = "2021" +publish = false +description = "EXPERIMENT: Quint de-risk spike for phase-1 validation (not part of the pallas workspace)" +license = "Apache-2.0" + +# Deliberately its own workspace: this crate is experiment evidence, excluded +# from the pallas workspace, its CI, and its publish surface. +[workspace] + +[features] +# Each feature seeds one deliberate defect into one rule of the slice so the +# model-based tests can demonstrate mutation catching. See EVIDENCE.md. +mutate-fee-floor = [] +mutate-size = [] +mutate-value = [] +mutate-collateral = [] + +[dev-dependencies] +# anyhow is referenced directly by quint-connect's switch! macro expansion +anyhow = "1" +quint-connect = "0.1.2" +serde = { version = "1", features = ["derive"] } diff --git a/experimental/quint-derisk/EVIDENCE.md b/experimental/quint-derisk/EVIDENCE.md new file mode 100644 index 000000000..7ddcd3f56 --- /dev/null +++ b/experimental/quint-derisk/EVIDENCE.md @@ -0,0 +1,158 @@ +# Quint de-risk experiment — evidence + +Phase 0b of the pallas phase-1 validation effort: can Quint serve as the +living spec and test oracle for the phase-1 rules? This file records the +evidence against the experiment's three pass criteria. The pass/fail ruling +is not made here — it belongs to the plan's owner at review time. + +## What ran + +| Component | Version | +|---|---| +| Quint CLI | 0.32.0 (`@informalsystems/quint`, via `bin/quint` npx shim) | +| quint-connect | 0.1.2 (crates.io) | +| rustc / cargo | 1.97.1 | + +- Model: `spec/conway_utxo.qnt` — Conway UTXO slice (fee floor, preservation + of value, size bounds, collateral bounds) as a state machine over a UTxO + set, with nine generator actions that each force one rule outcome. +- Implementation: `src/lib.rs` — the same checks behind a caller-supplied + `UtxoContext` trait (protocol parameters + input resolution supplied by the + caller, never owned by the validation function). +- Harness: `tests/mbt.rs` — a quint-connect driver replaying generated + traces. Transactions arrive verbatim as the model's nondet picks; verdicts + and UTxO transitions come from the spike; quint-connect diffs the full + state (UTxO set, tx counter, last verdict) against the model after every + step. + +Reproduce: + +```sh +cd experimental/quint-derisk +PATH="$PWD/bin:$PATH" cargo test # green: model and spike agree +PATH="$PWD/bin:$PATH" cargo test --features mutate-fee-floor # red: seeded defect caught +``` + +The MBT test is pinned to `seed = 0x2077`, 30 traces × 8 steps (270 replayed +steps including init). All runs below used that seed. + +## Criterion 1 — modelability + +Every check in the slice was expressible in Quint; the model typechecked on +the first attempt and simulates at ~27 traces/second. No unworkable gaps. +Workarounds and trims, all recorded in the spec header: + +| Semantics | Status in Quint | Workaround | +|---|---|---| +| Fee floor (`minFeeA·size + minFeeB`) | direct | — | +| Preservation of value | direct | lovelace-only values; multi-asset value maps would need a `Map[AssetId, int]` model (expressible, untested here) | +| Tx size bound | not modelable as bytes | size is an abstract per-tx attribute, supplied with the tx on both sides; the real byte count would be a caller-context input in phase 3 as well | +| Collateral bounds (count, 150% sufficiency) | direct | integer arithmetic written multiplication-only (`100·balance ≥ percent·fee`) to avoid division-rounding mismatches | +| Input resolution / bad inputs | direct | tx ids are a counter, not a body hash — hashing is outside Quint; a real harness would map hashes to abstract ids at the boundary | +| Check ordering | direct | first-failure short-circuit order is written identically on both sides and documented as part of the model/spike contract | + +Trims that narrow the slice's claimed scope (extrapolation below counts only +what was actually exercised): no collateral-return output or declared +total-collateral field, no ada-only/vkey-locked collateral constraints, no +min-utxo-value, no validity intervals, no mid-run parameter changes. + +## Criterion 2 — harness viability + +The driver holds implementation-side state only (a `BTreeMap` UTxO store fed +back through the `UtxoContext` trait); nothing in the harness re-implements a +rule or copies model state. Trace replay drives the spike through the same +boundary the phase-3 crate would expose. + +Rule coverage across the 30 pinned traces (each generator action forces one +rule outcome deterministically): + +| Action | Steps taken | Rule outcome exercised | +|---|---|---| +| submitValidTx | 27 | Accepted (state update: spend + create) | +| submitFeeTooSmallTx | 28 | FeeTooSmall | +| submitTooBigTx | 30 | TxTooBig | +| submitUnbalancedTx | 19 | ValueNotConserved | +| submitNoCollateralTx | 20 | NoCollateral | +| submitTooManyCollateralTx | 26 | TooManyCollateral | +| submitInsufficientCollateralTx | 28 | InsufficientCollateral | +| submitBadInputTx | 34 | BadInputs | +| submitEmptyInputsTx | 28 | EmptyInputs | + +### Mutation evidence + +Four cargo features each seed one deliberate defect into one rule +(`src/lib.rs`, marked `Seeded defect:`). With any one enabled, `cargo test +--test mbt` fails on a state diff; unmutated, all 270 steps pass. + +| Mutation | Seeded defect | Caught by | Divergence | +|---|---|---|---| +| `mutate-fee-floor` | fee floor off by one | trace 1, `submitFeeTooSmallTx` (fee = floor−1) | model: FeeTooSmall; mutant: Accepted (and UTxO/counter drift) | +| `mutate-size` | size limit 10× too lax | trace 1, `submitTooBigTx` (size 20000) | model: TxTooBig; mutant falls through to FeeTooSmall — caught as a verdict mismatch | +| `mutate-value` | conservation given ±1000 "tolerance" | trace 1, `submitUnbalancedTx` (delta +1) | model: ValueNotConserved; mutant: Accepted | +| `mutate-collateral` | percentage dropped from sufficiency check (+ count off-by-one) | trace 1, `submitInsufficientCollateralTx` | model: InsufficientCollateral; mutant: Accepted | + +Every mutation was caught within the first trace of the pinned seed. Full +failure logs show the exact step, nondet pick, and state diff (reproduce with +the commands above; quint-connect prints `Reproduce this error with +QUINT_SEED=0x2077`). + +## Criterion 3 — effort record and extrapolation + +Measured wall-clock for this slice, executed by an AI agent session +(2026-08-21, single session, times from the session log): + +| Part | Time | +|---|---| +| quint-connect API study (README, examples, source of the trace runner) | ~10 min | +| Quint model (9 generator actions + validation + transition), typecheck, first simulation | ~6 min | +| Rust spike (types, context trait, validate/apply, unit tests) | ~5 min | +| quint-connect harness (mirror types, driver, state extraction) | ~4 min | +| First green MBT run (one missing-dependency fix) | ~2 min | +| Mutations + evidence capture | ~8 min | +| **Total to reproducible evidence** | **~35 min** | + +The slice exercises 8 rejection rules plus the acceptance/state-update path +— call it 9 rule-units at ~4 min/rule-unit measured, after a fixed ~10 min +tooling ramp-up that does not recur. + +Extrapolation to the full Conway phase-1 rule set: the Conway ledger spec's +predicate-failure enumerations (UTXO, UTXOW, CERT/DELEG/POOL/GOVCERT, GOV, +LEDGER) total on the order of 60 checks. A naive linear extrapolation is +60 × 4 min ≈ 4 h of agent time for model + harness + mutation evidence. +That naive number needs honest multipliers: + +- **Multi-asset values** (value maps instead of ints) touch every arithmetic + rule: estimate 2–3× on the ~15 value-carrying checks. +- **Real transaction structure** (era CBOR, hashes, witnesses) does not enter + Quint — it stays behind the caller-context boundary — but the harness-side + mapping from real txs to model txs grows with every field the model gains: + estimate a further 1.5–2× on harness work as the model widens. +- **Certificate/governance state** brings multi-variable state (DReps, pools, + proposals) where trace generators need more care to reach interesting + states: the generator-design share of the work (about half the slice + effort) grows more than linearly there; budget 2× on those rule groups. +- **Model review**: this slice's model was written and checked by the same + session in minutes; a maintained living spec needs human review of the + model itself, which this measurement does not include. + +A defensible planning envelope from these numbers: **1.5–3 agent-days for a +full Conway phase-1 Quint model with a replay harness at this fidelity**, +plus the human review of the model that makes it a spec rather than a second +implementation. Whether that price (and the ongoing maintenance of ~60 +modeled rules) buys its weight as the phase-1 oracle is the ruling this +evidence exists to inform — it is not made here. + +## Tooling findings (quint-connect 0.1.2) + +- The `switch!` macro expansion references `anyhow` directly, so consumers + must add `anyhow` as their own dev-dependency — a macro-hygiene defect + worth an upstream report, trivial to work around. +- Composite nondet values work well: exposing a whole generated transaction + as a single record-valued nondet pick (`nondet vtx = Set({...}).oneOf()`) + gives the driver the tx verbatim and keeps generator logic out of Rust. + Distinct pick names per action avoid any ambiguity in the per-step + `nondetPicks` record. +- ITF deserialization (bigints, sets, record-keyed maps) mapped onto serde + types without friction. +- The crate's repo moved (informalsystems/quint-connect → + quint-co/quint-connect); docs links still resolve via redirect. diff --git a/experimental/quint-derisk/README.md b/experimental/quint-derisk/README.md new file mode 100644 index 000000000..d9f6cec2a --- /dev/null +++ b/experimental/quint-derisk/README.md @@ -0,0 +1,44 @@ +# Quint de-risk spike (EXPERIMENT) + +Phase 0b of the pallas phase-1 validation effort: a de-risk experiment +measuring whether a Quint executable spec, replayed against Rust with +[quint-connect](https://github.com/quint-co/quint-connect), can serve as the +living spec and test oracle for the phase-1 ledger rules. + +**This is experiment evidence, not product code.** The crate is excluded +from the pallas workspace (its own `[workspace]` root), never published, and +is *not* the phase-1 validation implementation — that will be a fresh start +under the phase-1 design. Whether this directory merges, is archived, or is +deleted is part of the experiment's ruling. + +## Contents + +- `spec/conway_utxo.qnt` — Quint model of a Conway UTXO slice: fee floor, + preservation of value, size bounds, collateral bounds. The model is the + oracle: it validates and applies every generated transaction. +- `src/lib.rs` — the same checks in Rust, behind a caller-supplied + `UtxoContext` boundary. Includes four `mutate-*` cargo features that each + seed one deliberate defect for mutation testing. +- `tests/mbt.rs` — quint-connect driver replaying model traces against the + spike, diffing full state every step. +- `EVIDENCE.md` — the experiment record: modelability notes, rule coverage, + mutation matrix, effort measurement and extrapolation. +- `bin/quint` — npx shim pinning the Quint CLI version. + +## Running + +Requires Rust and Node (for the Quint CLI via npx): + +```sh +cd experimental/quint-derisk +PATH="$PWD/bin:$PATH" cargo test # model and spike agree +PATH="$PWD/bin:$PATH" cargo test --features mutate-fee-floor # seeded defect: test fails +PATH="$PWD/bin:$PATH" QUINT_VERBOSE=1 cargo test -- --nocapture # show every step +``` + +Standalone model checks: + +```sh +bin/quint typecheck spec/conway_utxo.qnt +bin/quint run spec/conway_utxo.qnt --invariant nonNegativeUtxo --mbt +``` diff --git a/experimental/quint-derisk/bin/quint b/experimental/quint-derisk/bin/quint new file mode 100755 index 000000000..e9591780f --- /dev/null +++ b/experimental/quint-derisk/bin/quint @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +# npx shim so the quint-connect harness finds a pinned quint CLI on PATH. +exec npx --yes @informalsystems/quint@0.32.0 "$@" diff --git a/experimental/quint-derisk/spec/conway_utxo.qnt b/experimental/quint-derisk/spec/conway_utxo.qnt new file mode 100644 index 000000000..80e3339ea --- /dev/null +++ b/experimental/quint-derisk/spec/conway_utxo.qnt @@ -0,0 +1,301 @@ +// -*- mode: Bluespec; -*- +/** + * EXPERIMENT — Quint de-risk spike (phase 0b of pallas-phase1-validation). + * + * A Quint model of a slice of the Conway phase-1 UTXO rule: fee floor, + * preservation of value, transaction size bounds, and collateral bounds. + * Traces generated from this model are replayed against the Rust spike in + * `../src/lib.rs` via quint-connect (see `../tests/mbt.rs`). + * + * The model is the oracle: every submitted transaction is validated here and + * in Rust, and the two verdicts — plus the resulting UTxO set — must agree at + * every step. + * + * Deliberate trims from the full Conway UTXO rule (recorded for the + * extrapolation evidence in ../EVIDENCE.md): + * - values are lovelace only (no multi-assets, so no value-map arithmetic) + * - transaction size is an abstract attribute of the tx, not a byte count + * - no min-utxo-value (coinsPerUTxOByte), no output size/network checks + * - no validity interval, no protocol-parameter updates mid-run + * - collateral: no collateral-return output, no declared total-collateral + * field, no ada-only / vkey-locked constraints; collateral may overlap + * with spending inputs + * - tx ids are a counter, not a body hash + */ +module conway_utxo { + //// Protocol parameters — fixed for the experiment, mainnet-flavoured. + pure val minFeeA = 44 + pure val minFeeB = 155381 + pure val maxTxSize = 16384 + pure val collateralPercent = 150 + pure val maxCollateralInputs = 3 + + //// Transaction structure + + type TxIn = { txId: int, ix: int } + + type Tx = { + inputs: Set[TxIn], + outputs: List[int], + fee: int, + size: int, + isScripted: bool, + collateral: Set[TxIn], + } + + /// Outcome of validating one transaction. `NoTx` is the initial state + /// before any submission. + type Verdict = + | NoTx + | Accepted + | EmptyInputs + | BadInputs + | TxTooBig + | FeeTooSmall + | ValueNotConserved + | NoCollateral + | TooManyCollateral + | InsufficientCollateral + + //// State + + /// The live UTxO set: unspent outputs and their lovelace values. + var utxo: TxIn -> int + /// Abstract id assigned to the next accepted transaction. + var nextTxId: int + /// Verdict of the last submitted transaction. + var lastVerdict: Verdict + + //// Validation — the check order is part of the contract with the Rust + //// spike: first divergence wins, so both sides must short-circuit in the + //// same sequence. + + pure def minFee(tx: Tx): int = minFeeA * tx.size + minFeeB + + pure def sumValues(u: TxIn -> int, ins: Set[TxIn]): int = + ins.fold(0, (acc, i) => acc + u.get(i)) + + pure def produced(tx: Tx): int = + tx.outputs.foldl(0, (acc, o) => acc + o) + tx.fee + + pure def collateralVerdict(u: TxIn -> int, tx: Tx): Verdict = + if (tx.collateral.size() == 0) NoCollateral + else if (tx.collateral.size() > maxCollateralInputs) TooManyCollateral + else if (100 * sumValues(u, tx.collateral) < collateralPercent * tx.fee) + InsufficientCollateral + else Accepted + + pure def validate(u: TxIn -> int, tx: Tx): Verdict = + if (tx.inputs.size() == 0) EmptyInputs + else if (not(tx.inputs.union(tx.collateral).subseteq(u.keys()))) BadInputs + else if (tx.size > maxTxSize) TxTooBig + else if (tx.fee < minFee(tx)) FeeTooSmall + else if (sumValues(u, tx.inputs) != produced(tx)) ValueNotConserved + else if (tx.isScripted) collateralVerdict(u, tx) + else Accepted + + //// State transition + + pure def applyOutputs(u: TxIn -> int, outs: List[int], txId: int): TxIn -> int = + outs.indices().fold(u, (acc, i) => acc.put({ txId: txId, ix: i }, outs[i])) + + action applyTx(tx: Tx): bool = + val verdict = validate(utxo, tx) + if (verdict == Accepted) all { + utxo' = applyOutputs( + utxo.keys().exclude(tx.inputs).mapBy(k => utxo.get(k)), + tx.outputs, + nextTxId + ), + nextTxId' = nextTxId + 1, + lastVerdict' = Accepted, + } else all { + utxo' = utxo, + nextTxId' = nextTxId, + lastVerdict' = verdict, + } + + //// Transaction generators — one action per rule outcome, so every rule in + //// the slice is exercised many times per simulation. Each action exposes + //// the complete generated transaction as a single nondet pick (unique name + //// per action) that the Rust driver replays verbatim. + + pure val stdSize = 2000 + pure val stdFee = minFeeA * stdSize + minFeeB + pure val genesisAmount = 10000000 + + /// Inputs rich enough for a valid spend that leaves healthy outputs. + pure def spendables(u: TxIn -> int): Set[TxIn] = + u.keys().filter(k => u.get(k) >= 1000000) + + /// Inputs rich enough that rejected-tx generators never build a tx with + /// negative outputs. + pure def usable(u: TxIn -> int): Set[TxIn] = + u.keys().filter(k => u.get(k) >= 500000) + + pure def balancedOutputs(inVal: int, fee: int, nOuts: int): List[int] = + val change = inVal - fee + if (nOuts == 1) [change] else [change / 2, change - change / 2] + + /// Any 4 elements of a set (deterministic given the set). + pure def take4(s: Set[TxIn]): Set[TxIn] = + s.fold((0, Set()), (acc, x) => + if (acc._1 < 4) (acc._1 + 1, acc._2.union(Set(x))) else acc + )._2 + + action submitValidTx = all { + spendables(utxo).size() > 0, + nondet vIn = spendables(utxo).oneOf() + nondet vOuts = 1.to(2).oneOf() + nondet vScripted = Set(true, false).oneOf() + nondet vColl = spendables(utxo).oneOf() + nondet vtx = Set({ + inputs: Set(vIn), + outputs: balancedOutputs(utxo.get(vIn), stdFee, vOuts), + fee: stdFee, + size: stdSize, + isScripted: vScripted, + collateral: if (vScripted) Set(vColl) else Set(), + }).oneOf() + applyTx(vtx) + } + + action submitFeeTooSmallTx = all { + usable(utxo).size() > 0, + nondet fIn = usable(utxo).oneOf() + nondet fFee = Set(0, stdFee - 1).oneOf() + nondet ftx = Set({ + inputs: Set(fIn), + outputs: balancedOutputs(utxo.get(fIn), fFee, 1), + fee: fFee, + size: stdSize, + isScripted: false, + collateral: Set(), + }).oneOf() + applyTx(ftx) + } + + action submitTooBigTx = all { + usable(utxo).size() > 0, + nondet bIn = usable(utxo).oneOf() + nondet btx = Set({ + inputs: Set(bIn), + outputs: balancedOutputs(utxo.get(bIn), stdFee, 1), + fee: stdFee, + size: 20000, + isScripted: false, + collateral: Set(), + }).oneOf() + applyTx(btx) + } + + action submitUnbalancedTx = all { + usable(utxo).size() > 0, + nondet uIn = usable(utxo).oneOf() + nondet uDelta = Set(1, 999, -1000).oneOf() + nondet utx = Set({ + inputs: Set(uIn), + outputs: [utxo.get(uIn) - stdFee + uDelta], + fee: stdFee, + size: stdSize, + isScripted: false, + collateral: Set(), + }).oneOf() + applyTx(utx) + } + + action submitNoCollateralTx = all { + usable(utxo).size() > 0, + nondet nIn = usable(utxo).oneOf() + nondet ntx = Set({ + inputs: Set(nIn), + outputs: balancedOutputs(utxo.get(nIn), stdFee, 1), + fee: stdFee, + size: stdSize, + isScripted: true, + collateral: Set(), + }).oneOf() + applyTx(ntx) + } + + action submitTooManyCollateralTx = all { + usable(utxo).size() > 0, + utxo.keys().size() >= 4, + nondet mIn = usable(utxo).oneOf() + nondet mtx = Set({ + inputs: Set(mIn), + outputs: balancedOutputs(utxo.get(mIn), stdFee, 1), + fee: stdFee, + size: stdSize, + isScripted: true, + collateral: take4(utxo.keys()), + }).oneOf() + applyTx(mtx) + } + + /// Spend a whole input as fee, with itself as the only collateral: the + /// collateral balance is then always below collateralPercent (150%) of the + /// fee, so the collateral-sufficiency rule fires deterministically. + action submitInsufficientCollateralTx = all { + usable(utxo).size() > 0, + nondet iIn = usable(utxo).oneOf() + nondet itx = Set({ + inputs: Set(iIn), + outputs: [0], + fee: utxo.get(iIn), + size: stdSize, + isScripted: true, + collateral: Set(iIn), + }).oneOf() + applyTx(itx) + } + + action submitBadInputTx = all { + nondet gIx = 1.to(3).oneOf() + nondet gtx = Set({ + inputs: Set({ txId: 999999, ix: gIx }), + outputs: [1], + fee: stdFee, + size: stdSize, + isScripted: false, + collateral: Set(), + }).oneOf() + applyTx(gtx) + } + + action submitEmptyInputsTx = all { + nondet etx = Set({ + inputs: Set(), + outputs: [], + fee: 0, + size: stdSize, + isScripted: false, + collateral: Set(), + }).oneOf() + applyTx(etx) + } + + //// Machine + + action init = all { + utxo' = 0.to(4).map(i => { txId: 0, ix: i }).mapBy(_ => genesisAmount), + nextTxId' = 1, + lastVerdict' = NoTx, + } + + action step = any { + submitValidTx, + submitFeeTooSmallTx, + submitTooBigTx, + submitUnbalancedTx, + submitNoCollateralTx, + submitTooManyCollateralTx, + submitInsufficientCollateralTx, + submitBadInputTx, + submitEmptyInputsTx, + } + + //// Sanity invariant (not part of the slice; a guard on the generators) + + val nonNegativeUtxo = utxo.keys().forall(k => utxo.get(k) >= 0) +} diff --git a/experimental/quint-derisk/src/lib.rs b/experimental/quint-derisk/src/lib.rs new file mode 100644 index 000000000..d25109fce --- /dev/null +++ b/experimental/quint-derisk/src/lib.rs @@ -0,0 +1,284 @@ +//! EXPERIMENT — Quint de-risk spike (phase 0b of pallas-phase1-validation). +//! +//! A minimal slice of the Conway phase-1 UTXO checks — fee floor, +//! preservation of value, size bounds, collateral bounds — behind a +//! caller-supplied context boundary, written to be exercised by traces +//! generated from the Quint model in `spec/conway_utxo.qnt`. +//! +//! This crate is **evidence for an experiment**, not the phase-1 +//! implementation and not part of the pallas public surface: it is excluded +//! from the workspace, never published, and owes nothing to (and is owed +//! nothing by) the eventual `pallas-validate` successor. +//! +//! The check order mirrors the model and is part of the contract with it: +//! both sides short-circuit on the first failing rule. +//! +//! The `mutate-*` cargo features each seed one deliberate defect into one +//! rule. They exist so the model-based tests can demonstrate they catch +//! broken implementations; see `EVIDENCE.md`. + +use std::collections::{BTreeMap, BTreeSet}; + +pub type Lovelace = u64; + +/// A transaction input reference. The experiment abstracts tx ids to a +/// counter instead of a body hash. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] +pub struct TxIn { + pub tx_id: u64, + pub index: u64, +} + +/// The slice's view of a transaction: lovelace-only outputs, abstract size. +#[derive(Debug, Clone)] +pub struct Tx { + pub inputs: BTreeSet, + pub outputs: Vec, + pub fee: Lovelace, + pub size: u64, + pub is_scripted: bool, + pub collateral: BTreeSet, +} + +/// The protocol parameters the slice reads. +#[derive(Debug, Clone)] +pub struct PParams { + pub min_fee_a: u64, + pub min_fee_b: u64, + pub max_tx_size: u64, + pub collateral_percent: u64, + pub max_collateral_inputs: u64, +} + +/// Caller-supplied validation context (design tenet 1): the slice never owns +/// state — protocol parameters and UTxO resolution are the caller's to +/// provide. +pub trait UtxoContext { + fn pparams(&self) -> &PParams; + fn resolve(&self, input: &TxIn) -> Option; +} + +/// First rule violated by a transaction, in check order. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum ValidationError { + EmptyInputs, + BadInputs, + TxTooBig, + FeeTooSmall, + ValueNotConserved, + NoCollateral, + TooManyCollateral, + InsufficientCollateral, +} + +pub fn min_fee(tx: &Tx, pparams: &PParams) -> Lovelace { + pparams.min_fee_a * tx.size + pparams.min_fee_b +} + +/// Validate one transaction against the slice's rules, resolving inputs +/// through the caller's context. Checks run in the model's order and stop at +/// the first violation. +pub fn validate(tx: &Tx, ctx: &C) -> Result<(), ValidationError> { + let pparams = ctx.pparams(); + + if tx.inputs.is_empty() { + return Err(ValidationError::EmptyInputs); + } + + let mut consumed: Lovelace = 0; + for input in &tx.inputs { + match ctx.resolve(input) { + Some(value) => consumed += value, + None => return Err(ValidationError::BadInputs), + } + } + + let mut collateral_balance: Lovelace = 0; + for input in &tx.collateral { + match ctx.resolve(input) { + Some(value) => collateral_balance += value, + None => return Err(ValidationError::BadInputs), + } + } + + #[cfg(not(feature = "mutate-size"))] + let max_tx_size = pparams.max_tx_size; + // Seeded defect: size limit is never enforced in practice. + #[cfg(feature = "mutate-size")] + let max_tx_size = pparams.max_tx_size * 10; + if tx.size > max_tx_size { + return Err(ValidationError::TxTooBig); + } + + #[cfg(not(feature = "mutate-fee-floor"))] + let floor = min_fee(tx, pparams); + // Seeded defect: off-by-one on the fee floor. + #[cfg(feature = "mutate-fee-floor")] + let floor = min_fee(tx, pparams) - 1; + if tx.fee < floor { + return Err(ValidationError::FeeTooSmall); + } + + let produced: Lovelace = tx.outputs.iter().sum::() + tx.fee; + #[cfg(not(feature = "mutate-value"))] + let conserved = consumed == produced; + // Seeded defect: value preservation with a "rounding tolerance". + #[cfg(feature = "mutate-value")] + let conserved = consumed.abs_diff(produced) <= 1000; + if !conserved { + return Err(ValidationError::ValueNotConserved); + } + + if tx.is_scripted { + if tx.collateral.is_empty() { + return Err(ValidationError::NoCollateral); + } + + #[cfg(not(feature = "mutate-collateral"))] + let max_collateral = pparams.max_collateral_inputs; + // Seeded defect: off-by-one on the collateral input count. + #[cfg(feature = "mutate-collateral")] + let max_collateral = pparams.max_collateral_inputs + 1; + if tx.collateral.len() as u64 > max_collateral { + return Err(ValidationError::TooManyCollateral); + } + + #[cfg(not(feature = "mutate-collateral"))] + let sufficient = 100 * collateral_balance >= pparams.collateral_percent * tx.fee; + // Seeded defect: the percentage is forgotten — collateral only has to + // cover the fee itself. + #[cfg(feature = "mutate-collateral")] + let sufficient = collateral_balance >= tx.fee; + if !sufficient { + return Err(ValidationError::InsufficientCollateral); + } + } + + Ok(()) +} + +/// Apply a validated transaction to a UTxO store: spend the inputs, create +/// the outputs under the given tx id. Collateral is untouched — the slice +/// models phase-1 success only. +pub fn apply(tx: &Tx, tx_id: u64, utxos: &mut BTreeMap) { + for input in &tx.inputs { + utxos.remove(input); + } + for (index, value) in tx.outputs.iter().enumerate() { + utxos.insert( + TxIn { + tx_id, + index: index as u64, + }, + *value, + ); + } +} + +#[cfg(test)] +mod tests { + use super::*; + + struct Ctx { + pparams: PParams, + utxos: BTreeMap, + } + + impl UtxoContext for Ctx { + fn pparams(&self) -> &PParams { + &self.pparams + } + + fn resolve(&self, input: &TxIn) -> Option { + self.utxos.get(input).copied() + } + } + + fn ctx() -> Ctx { + Ctx { + pparams: PParams { + min_fee_a: 44, + min_fee_b: 155381, + max_tx_size: 16384, + collateral_percent: 150, + max_collateral_inputs: 3, + }, + utxos: BTreeMap::from([(TxIn { tx_id: 0, index: 0 }, 10_000_000)]), + } + } + + fn valid_tx() -> Tx { + let fee = 44 * 2000 + 155381; + Tx { + inputs: BTreeSet::from([TxIn { tx_id: 0, index: 0 }]), + outputs: vec![10_000_000 - fee], + fee, + size: 2000, + is_scripted: false, + collateral: BTreeSet::new(), + } + } + + #[test] + fn accepts_a_valid_tx() { + assert_eq!(validate(&valid_tx(), &ctx()), Ok(())); + } + + #[test] + fn rejects_fee_below_floor() { + let mut tx = valid_tx(); + tx.fee -= 1; + let expected = if cfg!(feature = "mutate-fee-floor") { + // Under the seeded defect the floor is off by one, and with the + // fee lowered the value check fires instead (unless that check is + // also mutated away). + Err(ValidationError::ValueNotConserved) + } else { + Err(ValidationError::FeeTooSmall) + }; + assert_eq!(validate(&tx, &ctx()), expected); + } + + #[test] + fn rejects_oversized_tx() { + let mut tx = valid_tx(); + tx.size = 20000; + let expected = if cfg!(feature = "mutate-size") { + Err(ValidationError::FeeTooSmall) + } else { + Err(ValidationError::TxTooBig) + }; + assert_eq!(validate(&tx, &ctx()), expected); + } + + #[test] + fn rejects_unbalanced_tx() { + let mut tx = valid_tx(); + tx.outputs[0] += 1; + let expected = if cfg!(feature = "mutate-value") { + Ok(()) + } else { + Err(ValidationError::ValueNotConserved) + }; + assert_eq!(validate(&tx, &ctx()), expected); + } + + #[test] + fn rejects_scripted_tx_without_collateral() { + let mut tx = valid_tx(); + tx.is_scripted = true; + assert_eq!(validate(&tx, &ctx()), Err(ValidationError::NoCollateral)); + } + + #[test] + fn apply_spends_and_creates() { + let mut utxos = ctx().utxos; + let tx = valid_tx(); + apply(&tx, 1, &mut utxos); + assert!(!utxos.contains_key(&TxIn { tx_id: 0, index: 0 })); + assert_eq!( + utxos.get(&TxIn { tx_id: 1, index: 0 }), + Some(&tx.outputs[0]) + ); + } +} diff --git a/experimental/quint-derisk/tests/mbt.rs b/experimental/quint-derisk/tests/mbt.rs new file mode 100644 index 000000000..a868b0733 --- /dev/null +++ b/experimental/quint-derisk/tests/mbt.rs @@ -0,0 +1,219 @@ +//! Model-based tests: replay traces generated from `spec/conway_utxo.qnt` +//! against the Rust spike via quint-connect. +//! +//! The driver holds the implementation-side ledger state (UTxO store + +//! protocol parameters) and is itself the caller-supplied `UtxoContext` for +//! the spike. Nothing here re-implements a rule: transactions come verbatim +//! from the model's nondet picks, verdicts and state transitions come from +//! the spike, and quint-connect compares the resulting state against the +//! model after every step. +//! +//! Requires the `quint` CLI on PATH (see `bin/quint` for an npx shim): +//! +//! ```text +//! PATH="$PWD/bin:$PATH" cargo test --test mbt +//! ``` + +use conway_utxo_quint_spike::*; +use quint_connect::*; +use serde::Deserialize; +use std::collections::{BTreeMap, BTreeSet}; + +/// Mirror of the model's `TxIn` record. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Deserialize)] +struct QTxIn { + #[serde(rename = "txId")] + tx_id: u64, + ix: u64, +} + +impl From for TxIn { + fn from(q: QTxIn) -> Self { + TxIn { + tx_id: q.tx_id, + index: q.ix, + } + } +} + +impl From for QTxIn { + fn from(t: TxIn) -> Self { + QTxIn { + tx_id: t.tx_id, + ix: t.index, + } + } +} + +/// Mirror of the model's `Tx` record. +#[derive(Debug, Deserialize)] +struct QTx { + inputs: BTreeSet, + outputs: Vec, + fee: u64, + size: u64, + #[serde(rename = "isScripted")] + is_scripted: bool, + collateral: BTreeSet, +} + +impl From for Tx { + fn from(q: QTx) -> Self { + Tx { + inputs: q.inputs.into_iter().map(Into::into).collect(), + outputs: q.outputs, + fee: q.fee, + size: q.size, + is_scripted: q.is_scripted, + collateral: q.collateral.into_iter().map(Into::into).collect(), + } + } +} + +/// Mirror of the model's `Verdict` sum type. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Deserialize)] +#[serde(tag = "tag")] +enum QVerdict { + NoTx, + Accepted, + EmptyInputs, + BadInputs, + TxTooBig, + FeeTooSmall, + ValueNotConserved, + NoCollateral, + TooManyCollateral, + InsufficientCollateral, +} + +impl From for QVerdict { + fn from(e: ValidationError) -> Self { + match e { + ValidationError::EmptyInputs => QVerdict::EmptyInputs, + ValidationError::BadInputs => QVerdict::BadInputs, + ValidationError::TxTooBig => QVerdict::TxTooBig, + ValidationError::FeeTooSmall => QVerdict::FeeTooSmall, + ValidationError::ValueNotConserved => QVerdict::ValueNotConserved, + ValidationError::NoCollateral => QVerdict::NoCollateral, + ValidationError::TooManyCollateral => QVerdict::TooManyCollateral, + ValidationError::InsufficientCollateral => QVerdict::InsufficientCollateral, + } + } +} + +struct LedgerDriver { + pparams: PParams, + utxos: BTreeMap, + next_tx_id: u64, + last_verdict: QVerdict, +} + +impl LedgerDriver { + fn new() -> Self { + Self { + // Must match the model's protocol parameter constants. + pparams: PParams { + min_fee_a: 44, + min_fee_b: 155381, + max_tx_size: 16384, + collateral_percent: 150, + max_collateral_inputs: 3, + }, + utxos: BTreeMap::new(), + next_tx_id: 1, + last_verdict: QVerdict::NoTx, + } + } + + fn init(&mut self) { + // Must match the model's `init`: five genesis outputs of 10M each. + self.utxos = (0..5) + .map(|ix| { + ( + TxIn { + tx_id: 0, + index: ix, + }, + 10_000_000, + ) + }) + .collect(); + self.next_tx_id = 1; + self.last_verdict = QVerdict::NoTx; + } + + fn submit(&mut self, qtx: QTx) { + let tx: Tx = qtx.into(); + match validate(&tx, self) { + Ok(()) => { + apply(&tx, self.next_tx_id, &mut self.utxos); + self.next_tx_id += 1; + self.last_verdict = QVerdict::Accepted; + } + Err(e) => self.last_verdict = e.into(), + } + } +} + +impl UtxoContext for LedgerDriver { + fn pparams(&self) -> &PParams { + &self.pparams + } + + fn resolve(&self, input: &TxIn) -> Option { + self.utxos.get(input).copied() + } +} + +/// Mirror of the model's state variables, compared after every step. +#[derive(Debug, PartialEq, Deserialize)] +struct LedgerState { + utxo: BTreeMap, + #[serde(rename = "nextTxId")] + next_tx_id: u64, + #[serde(rename = "lastVerdict")] + last_verdict: QVerdict, +} + +impl State for LedgerState { + fn from_driver(driver: &LedgerDriver) -> Result { + Ok(Self { + utxo: driver + .utxos + .iter() + .map(|(k, v)| ((*k).into(), *v)) + .collect(), + next_tx_id: driver.next_tx_id, + last_verdict: driver.last_verdict, + }) + } +} + +impl Driver for LedgerDriver { + type State = LedgerState; + + fn step(&mut self, step: &Step) -> Result { + switch!(step { + init => self.init(), + submitValidTx(vtx: QTx) => self.submit(vtx), + submitFeeTooSmallTx(ftx: QTx) => self.submit(ftx), + submitTooBigTx(btx: QTx) => self.submit(btx), + submitUnbalancedTx(utx: QTx) => self.submit(utx), + submitNoCollateralTx(ntx: QTx) => self.submit(ntx), + submitTooManyCollateralTx(mtx: QTx) => self.submit(mtx), + submitInsufficientCollateralTx(itx: QTx) => self.submit(itx), + submitBadInputTx(gtx: QTx) => self.submit(gtx), + submitEmptyInputsTx(etx: QTx) => self.submit(etx), + }) + } +} + +#[quint_run( + spec = "spec/conway_utxo.qnt", + max_samples = 30, + max_steps = 8, + seed = "0x2077" +)] +fn conway_utxo_traces() -> impl Driver { + LedgerDriver::new() +} From 7ac1a133ac7f5fbacbb63f04554889e7d9a591ec Mon Sep 17 00:00:00 2001 From: Santiago Date: Fri, 21 Aug 2026 17:35:44 -0300 Subject: [PATCH 2/3] chore(experimental): drop bare section-label comments from the Quint spec Comment-only sweep to the TxPipe comment standard: the four bare section labels named nothing their following items don't name themselves. Prose-carrying headers stay. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01X15KSXtdC7jqv1QmV9dYC2 --- experimental/quint-derisk/spec/conway_utxo.qnt | 8 -------- 1 file changed, 8 deletions(-) diff --git a/experimental/quint-derisk/spec/conway_utxo.qnt b/experimental/quint-derisk/spec/conway_utxo.qnt index 80e3339ea..e786c877e 100644 --- a/experimental/quint-derisk/spec/conway_utxo.qnt +++ b/experimental/quint-derisk/spec/conway_utxo.qnt @@ -30,8 +30,6 @@ module conway_utxo { pure val collateralPercent = 150 pure val maxCollateralInputs = 3 - //// Transaction structure - type TxIn = { txId: int, ix: int } type Tx = { @@ -57,8 +55,6 @@ module conway_utxo { | TooManyCollateral | InsufficientCollateral - //// State - /// The live UTxO set: unspent outputs and their lovelace values. var utxo: TxIn -> int /// Abstract id assigned to the next accepted transaction. @@ -94,8 +90,6 @@ module conway_utxo { else if (tx.isScripted) collateralVerdict(u, tx) else Accepted - //// State transition - pure def applyOutputs(u: TxIn -> int, outs: List[int], txId: int): TxIn -> int = outs.indices().fold(u, (acc, i) => acc.put({ txId: txId, ix: i }, outs[i])) @@ -275,8 +269,6 @@ module conway_utxo { applyTx(etx) } - //// Machine - action init = all { utxo' = 0.to(4).map(i => { txId: 0, ix: i }).mapBy(_ => genesisAmount), nextTxId' = 1, From 446e8dfde2c8d50ba1da78c796682f7b1e403435 Mon Sep 17 00:00:00 2001 From: Santiago Date: Fri, 21 Aug 2026 17:35:44 -0300 Subject: [PATCH 3/3] chore(experimental): track the spike's Cargo.lock and document --locked MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The spike is its own workspace root, so its lockfile pins the quint-connect/serde dependency tree the evidence was produced with — the same drift the root workspace's CI currently suffers from. A gitignore negation keeps the exception local to the experiment. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01X15KSXtdC7jqv1QmV9dYC2 --- experimental/quint-derisk/.gitignore | 1 + experimental/quint-derisk/Cargo.lock | 1057 ++++++++++++++++++++++++ experimental/quint-derisk/README.md | 6 +- experimental/quint-derisk/tests/mbt.rs | 2 +- 4 files changed, 1062 insertions(+), 4 deletions(-) create mode 100644 experimental/quint-derisk/Cargo.lock diff --git a/experimental/quint-derisk/.gitignore b/experimental/quint-derisk/.gitignore index ea8c4bf7f..8ce0a8f20 100644 --- a/experimental/quint-derisk/.gitignore +++ b/experimental/quint-derisk/.gitignore @@ -1 +1,2 @@ /target +!Cargo.lock diff --git a/experimental/quint-derisk/Cargo.lock b/experimental/quint-derisk/Cargo.lock new file mode 100644 index 000000000..35feca99d --- /dev/null +++ b/experimental/quint-derisk/Cargo.lock @@ -0,0 +1,1057 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "android_system_properties" +version = "0.1.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae221649c9976a6f6c56ae1facf410f3ddb33cc661c4b7b61020a912d4237fbc" +dependencies = [ + "libc", +] + +[[package]] +name = "anyhow" +version = "1.0.104" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470" + +[[package]] +name = "autocfg" +version = "1.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" + +[[package]] +name = "base64" +version = "0.22.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6" + +[[package]] +name = "bitflags" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" + +[[package]] +name = "bitflags" +version = "2.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b588b76d00fde79687d7646a9b5bdf3cc0f655e0bbd080335a95d7e96f3587da" + +[[package]] +name = "bs58" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf88ba1141d185c399bee5288d850d63b8369520c1eafc32a0430b5b6c287bf4" +dependencies = [ + "tinyvec", +] + +[[package]] +name = "bumpalo" +version = "3.20.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649" + +[[package]] +name = "cc" +version = "1.4.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ad534f4357a5264cce5019c989cf66a4f0dc4e0d1b1d15f8aacec0ff7360273" +dependencies = [ + "find-msvc-tools", + "shlex", +] + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "chrono" +version = "0.4.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1aa79e62e7697b8e29b513a68abacf485adcd1fe8284a4316c5ae868e6633327" +dependencies = [ + "iana-time-zone", + "num-traits", + "serde", + "windows-link", +] + +[[package]] +name = "colored" +version = "3.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34" +dependencies = [ + "windows-sys", +] + +[[package]] +name = "conway-utxo-quint-spike" +version = "0.0.0" +dependencies = [ + "anyhow", + "quint-connect", + "serde", +] + +[[package]] +name = "core-foundation-sys" +version = "0.8.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" + +[[package]] +name = "darling" +version = "0.23.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "25ae13da2f202d56bd7f91c25fba009e7717a1e4a1cc98a76d844b65ae912e9d" +dependencies = [ + "darling_core", + "darling_macro", +] + +[[package]] +name = "darling_core" +version = "0.23.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9865a50f7c335f53564bb694ef660825eb8610e0a53d3e11bf1b0d3df31e03b0" +dependencies = [ + "ident_case", + "proc-macro2", + "quote", + "strsim", + "syn 2.0.119", +] + +[[package]] +name = "darling_macro" +version = "0.23.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3984ec7bd6cfa798e62b4a642426a5be0e68f9401cfc2a01e3fa9ea2fcdb8d" +dependencies = [ + "darling_core", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "dashu-base" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "993b95dc1b248e3f5747dcb017a41d6e75853a2e5ee4504f7d537c5b8dffdae4" + +[[package]] +name = "dashu-int" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49c05a0d5cb0b39fcc87c46432fdac24b90dce239857c7f6b798be4ffc3c42c6" +dependencies = [ + "cfg-if", + "dashu-base", + "num-modular", + "num-order", + "rustversion", + "serde", + "static_assertions", +] + +[[package]] +name = "defmt" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2953bfe4f93bbd20cc71198842756f77d161884c99ebbabc41d80231ded88d1" +dependencies = [ + "bitflags 1.3.2", + "defmt-macros", +] + +[[package]] +name = "defmt-macros" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bad9c72e7ca2137e0dc3813245a0d282fd6daad32fd800af018306a9169b5fe8" +dependencies = [ + "defmt-parser", + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "defmt-parser" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "10d60334b3b2e7c9d91ef8150abfb6fa4c1c39ebbcf4a81c2e346aad939fee3e" +dependencies = [ + "thiserror", +] + +[[package]] +name = "deranged" +version = "0.5.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7cd812cc2bc1d69d4764bd80df88b4317eaef9e773c75226407d9bc0876b211c" +dependencies = [ + "serde_core", +] + +[[package]] +name = "dyn-clone" +version = "1.0.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d0881ea181b1df73ff77ffaaf9c7544ecc11e82fba9b5f27b262a3c73a332555" + +[[package]] +name = "equivalent" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" + +[[package]] +name = "errno" +version = "0.3.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" +dependencies = [ + "libc", + "windows-sys", +] + +[[package]] +name = "fastrand" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da7c62ceae207dd37ea5b845da6a0696c799f85e97da1ab5b7910be3c1c80223" + +[[package]] +name = "find-msvc-tools" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d45db016d36b838f563236e9193d0ee6ce38f3f68b6c94e914b4929c96bbb890" + +[[package]] +name = "futures-core" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "92d699e522242e69e3003b94ecc1f960f3a5e015aa7c5d7486e65ad01dd94f5e" + +[[package]] +name = "futures-task" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cd417de3d1d015fc3bfd2b1ea46dfc7bab72ef86f1cc7cc9c78e728b34a6d1fd" + +[[package]] +name = "futures-util" +version = "0.3.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0d50a92467f8ba5dd6e3ee5d4bd04d73ab2e4e1c44474a0674821dfce14b79bc" +dependencies = [ + "futures-core", + "futures-task", + "pin-project-lite", + "slab", +] + +[[package]] +name = "getrandom" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" +dependencies = [ + "cfg-if", + "libc", + "r-efi 5.3.0", + "wasip2", +] + +[[package]] +name = "getrandom" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "300e883d756b2e4ec94e02791f39b04b522276138852cfc41d9fb7e904106099" +dependencies = [ + "cfg-if", + "libc", + "r-efi 6.0.0", +] + +[[package]] +name = "hashbrown" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" + +[[package]] +name = "hashbrown" +version = "0.17.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" + +[[package]] +name = "hex" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70" + +[[package]] +name = "iana-time-zone" +version = "0.1.65" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e31bc9ad994ba00e440a8aa5c9ef0ec67d5cb5e5cb0cc7f8b744a35b389cc470" +dependencies = [ + "android_system_properties", + "core-foundation-sys", + "iana-time-zone-haiku", + "js-sys", + "log", + "wasm-bindgen", + "windows-core", +] + +[[package]] +name = "iana-time-zone-haiku" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f31827a206f56af32e590ba56d5d2d085f558508192593743f16b2306495269f" +dependencies = [ + "cc", +] + +[[package]] +name = "ident_case" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39" + +[[package]] +name = "indexmap" +version = "1.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99" +dependencies = [ + "autocfg", + "hashbrown 0.12.3", + "serde", +] + +[[package]] +name = "indexmap" +version = "2.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" +dependencies = [ + "equivalent", + "hashbrown 0.17.1", + "serde", + "serde_core", +] + +[[package]] +name = "itf" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5d620b7b3d17650581da9208d1240baaff4ee33decff1c7782bdb9b4cab71c20" +dependencies = [ + "dashu-int", + "serde", + "serde_json", + "serde_with", +] + +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + +[[package]] +name = "jiff" +version = "0.2.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "668b7183bd07af9a4885f5c35b0cc5c83c4607a913c16b7e17291832910d2dcc" +dependencies = [ + "defmt", + "jiff-core", + "jiff-static", + "jiff-tzdb-platform", + "log", + "portable-atomic", + "portable-atomic-util", + "serde_core", + "windows-link", +] + +[[package]] +name = "jiff-core" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7feca88439efe53da3754500c1851dedf3cb36c524dd5cf8225cc0794de95d09" +dependencies = [ + "defmt", +] + +[[package]] +name = "jiff-static" +version = "0.2.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3a69dcb3a21cfb32ce1cd056169337ca284af0766dd766e7878819b251a49204" +dependencies = [ + "jiff-core", + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "jiff-tzdb" +version = "0.1.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "142bd39932ad231f10513df9ab62661fead8719872150b7ad02a2df79f4e141e" + +[[package]] +name = "jiff-tzdb-platform" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "875a5a69ac2bab1a891711cf5eccbec1ce0341ea805560dcd90b7a2e925132e8" +dependencies = [ + "jiff-tzdb", +] + +[[package]] +name = "js-sys" +version = "0.3.104" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e0c1080212aad755ea003d18543e8768dd432c48819efd73a7bf1e39b7a5a3a" +dependencies = [ + "cfg-if", + "futures-util", + "wasm-bindgen", +] + +[[package]] +name = "libc" +version = "0.2.189" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2" + +[[package]] +name = "linux-raw-sys" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53" + +[[package]] +name = "log" +version = "0.4.33" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ceec5bc11778974d1bcb055b18002eba7f4b3518b6a0081b3af5f21666da9ad" + +[[package]] +name = "memchr" +version = "2.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" + +[[package]] +name = "num-conv" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "521739c6d2bac4aa25192232afe6841231376b2b26d4d9fae5ecf8ca5772e441" + +[[package]] +name = "num-modular" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bd8e500409e6cd603b03e477c26a6caecdc27ac58979a53e881c75eafc079f44" + +[[package]] +name = "num-order" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "537b596b97c40fcf8056d153049eb22f481c17ebce72a513ec9286e4986d1bb6" +dependencies = [ + "num-modular", +] + +[[package]] +name = "num-traits" +version = "0.2.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" +dependencies = [ + "autocfg", +] + +[[package]] +name = "once_cell" +version = "1.21.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" + +[[package]] +name = "pin-project-lite" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" + +[[package]] +name = "portable-atomic" +version = "1.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "05c8b63e8d9609db387f0324918f81d68fe27748f084ef092fb35954d0539a85" + +[[package]] +name = "portable-atomic-util" +version = "0.2.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2a106d1259c23fac8e543272398ae0e3c0b8d33c88ed73d0cc71b0f1d902618" +dependencies = [ + "portable-atomic", +] + +[[package]] +name = "powerfmt" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" + +[[package]] +name = "ppv-lite86" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" +dependencies = [ + "zerocopy", +] + +[[package]] +name = "proc-macro2" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quint-connect" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67a4e156a3d4580b73eff41805d3237c909f96388158b3eed12afaa4f619d61c" +dependencies = [ + "anyhow", + "colored", + "itf", + "quint-connect-macros", + "rand", + "serde", + "serde_json", + "similar", + "tempfile", + "version_check", +] + +[[package]] +name = "quint-connect-macros" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "814c6e076fa655b78d7127fda492f3fa980b8827fda16c33d891b57c8ccd735f" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "quote" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "r-efi" +version = "5.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" + +[[package]] +name = "r-efi" +version = "6.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" + +[[package]] +name = "rand" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9ef1d0d795eb7d84685bca4f72f3649f064e6641543d3a8c415898726a57b41" +dependencies = [ + "rand_chacha", + "rand_core", +] + +[[package]] +name = "rand_chacha" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" +dependencies = [ + "ppv-lite86", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" +dependencies = [ + "getrandom 0.3.4", +] + +[[package]] +name = "ref-cast" +version = "1.0.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e440fb4e4b4147295338efb76001ab9e4efc0e5839df2c47fc5ac2381d365c3" +dependencies = [ + "ref-cast-impl", +] + +[[package]] +name = "ref-cast-impl" +version = "1.0.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "92ecd8964f8453721699a1ed72037b0db49ce2f5a5138486ee89bed6f67cdf3a" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.3", +] + +[[package]] +name = "rustix" +version = "1.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6fe4565b9518b83ef4f91bb47ce29620ca828bd32cb7e408f0062e9930ba190" +dependencies = [ + "bitflags 2.13.1", + "errno", + "libc", + "linux-raw-sys", + "windows-sys", +] + +[[package]] +name = "rustversion" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf54715a573b99ac80df0bc206da022bcd442c974952c7b9720069370852e21f" + +[[package]] +name = "schemars" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4cd191f9397d57d581cddd31014772520aa448f65ef991055d7f61582c65165f" +dependencies = [ + "dyn-clone", + "ref-cast", + "serde", + "serde_json", +] + +[[package]] +name = "schemars" +version = "1.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "687274d293b6cdc6e73e0fee520bf2049650090d7164f87672d212a3c530cf4a" +dependencies = [ + "dyn-clone", + "ref-cast", + "serde", + "serde_json", +] + +[[package]] +name = "serde" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba" +dependencies = [ + "serde_core", + "serde_derive", +] + +[[package]] +name = "serde_core" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.3", +] + +[[package]] +name = "serde_json" +version = "1.0.151" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14" +dependencies = [ + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + +[[package]] +name = "serde_with" +version = "3.22.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ee78f1fbe43ac4a0e47aadb3dbd357b69eb0d3793e948624cd03dd2750ab1c0a" +dependencies = [ + "base64", + "bs58", + "chrono", + "hex", + "indexmap 1.9.3", + "indexmap 2.14.0", + "jiff", + "schemars 0.9.0", + "schemars 1.2.2", + "serde_core", + "serde_json", + "serde_with_macros", + "time", +] + +[[package]] +name = "serde_with_macros" +version = "3.22.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8705578779c2b6bd90d84d66eb2e206b708b1a4d7b9f17641b293545bf1c7e46" +dependencies = [ + "darling", + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "shlex" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8fadd59c855ef2080decdef8ff161eb6661b86933c9d82e5ba29dc602a55aba" + +[[package]] +name = "similar" +version = "2.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbbb5d9659141646ae647b42fe094daf6c6192d1620870b449d9557f748b2daa" + +[[package]] +name = "slab" +version = "0.4.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" + +[[package]] +name = "static_assertions" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" + +[[package]] +name = "strsim" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" + +[[package]] +name = "syn" +version = "2.0.119" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "3.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "tempfile" +version = "3.27.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd" +dependencies = [ + "fastrand", + "getrandom 0.4.3", + "once_cell", + "rustix", + "windows-sys", +] + +[[package]] +name = "thiserror" +version = "2.0.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec86235f5fcc2a73650310756d2ac5b138a5780bbbdfae3eeccec992c435ba4f" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "2.0.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bc04cd3e1236dd4a98afca4569f2deb3f120e5422a4023be2cb683f8486292af" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.3", +] + +[[package]] +name = "time" +version = "0.3.55" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cdb87b95ec50ddfa440816d227a17b2ccbdda963a316a727fda0fc4334f7d134" +dependencies = [ + "deranged", + "num-conv", + "powerfmt", + "serde_core", + "time-core", + "time-macros", +] + +[[package]] +name = "time-core" +version = "0.1.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9e1c906769ad99c88eaa54e728060edef082f8e358ff32030cb7c7d315e81109" + +[[package]] +name = "time-macros" +version = "0.2.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e689342a48d2ea927c87ea50cabf8594854bf940e9310208848d680d668ed85" +dependencies = [ + "num-conv", + "time-core", +] + +[[package]] +name = "tinyvec" +version = "1.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bb4ebadaa0af04fab11ae01eb5f9fdb5f9c5b875506e210e71c07873528baa7f" +dependencies = [ + "tinyvec_macros", +] + +[[package]] +name = "tinyvec_macros" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1f3ccbac311fea05f86f61904b462b55fb3df8837a366dfc601a0161d0532f20" + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + +[[package]] +name = "wasip2" +version = "1.0.4+wasi-0.2.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b67efb37e106e55ce722a510d6b5f9c17f083e5fc79afc2badeb12cc313d9487" +dependencies = [ + "wit-bindgen", +] + +[[package]] +name = "wasm-bindgen" +version = "0.2.127" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1b70935747edd64d89de3efa29d73789b806c15798f8e7dca4d8ac356b50ce70" +dependencies = [ + "cfg-if", + "once_cell", + "rustversion", + "wasm-bindgen-macro", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-macro" +version = "0.2.127" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77775f8f3f7217702089053b94958f8f54061a3f663417df76e19cbdcca29bc1" +dependencies = [ + "quote", + "wasm-bindgen-macro-support", +] + +[[package]] +name = "wasm-bindgen-macro-support" +version = "0.2.127" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e11d33f857dc2fb11b8bc75aee111aa9cbeb12cd9f25efd3d4c2a3dd4e235284" +dependencies = [ + "bumpalo", + "proc-macro2", + "quote", + "syn 2.0.119", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-shared" +version = "0.2.127" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7ef64dbcc55df09c7e5a46182d181c2cfa3e925f3da937ea764728b4bbb9dcbf" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "windows-core" +version = "0.62.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b8e83a14d34d0623b51dce9581199302a221863196a1dde71a7663a4c2be9deb" +dependencies = [ + "windows-implement", + "windows-interface", + "windows-link", + "windows-result", + "windows-strings", +] + +[[package]] +name = "windows-implement" +version = "0.60.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "053e2e040ab57b9dc951b72c264860db7eb3b0200ba345b4e4c3b14f67855ddf" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "windows-interface" +version = "0.59.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f316c4a2570ba26bbec722032c4099d8c8bc095efccdc15688708623367e358" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "windows-link" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" + +[[package]] +name = "windows-result" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7781fa89eaf60850ac3d2da7af8e5242a5ea78d1a11c49bf2910bb5a73853eb5" +dependencies = [ + "windows-link", +] + +[[package]] +name = "windows-strings" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7837d08f69c77cf6b07689544538e017c1bfcf57e34b4c0ff58e6c2cd3b37091" +dependencies = [ + "windows-link", +] + +[[package]] +name = "windows-sys" +version = "0.61.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae137229bcbd6cdf0f7b80a31df61766145077ddf49416a728b02cb3921ff3fc" +dependencies = [ + "windows-link", +] + +[[package]] +name = "wit-bindgen" +version = "0.57.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" + +[[package]] +name = "zerocopy" +version = "0.8.56" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "556764e583adb45a9f8d413c2a147fa7e8d821e48e12b14fd560b607998b75eb" +dependencies = [ + "zerocopy-derive", +] + +[[package]] +name = "zerocopy-derive" +version = "0.8.56" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2ab42fc20575779bd240faa45f94a74256f755c0fa9e89f0ede20d91d0cdfc1" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + +[[package]] +name = "zmij" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29666d0abbfad1e3dc4dcf6144730dd3a3ab225bbbdac83319345b1b44ccfc1b" diff --git a/experimental/quint-derisk/README.md b/experimental/quint-derisk/README.md index d9f6cec2a..816f06e95 100644 --- a/experimental/quint-derisk/README.md +++ b/experimental/quint-derisk/README.md @@ -31,9 +31,9 @@ Requires Rust and Node (for the Quint CLI via npx): ```sh cd experimental/quint-derisk -PATH="$PWD/bin:$PATH" cargo test # model and spike agree -PATH="$PWD/bin:$PATH" cargo test --features mutate-fee-floor # seeded defect: test fails -PATH="$PWD/bin:$PATH" QUINT_VERBOSE=1 cargo test -- --nocapture # show every step +PATH="$PWD/bin:$PATH" cargo test --locked # model and spike agree +PATH="$PWD/bin:$PATH" cargo test --locked --features mutate-fee-floor # seeded defect: test fails +PATH="$PWD/bin:$PATH" QUINT_VERBOSE=1 cargo test --locked -- --nocapture # show every step ``` Standalone model checks: diff --git a/experimental/quint-derisk/tests/mbt.rs b/experimental/quint-derisk/tests/mbt.rs index a868b0733..319f13c09 100644 --- a/experimental/quint-derisk/tests/mbt.rs +++ b/experimental/quint-derisk/tests/mbt.rs @@ -11,7 +11,7 @@ //! Requires the `quint` CLI on PATH (see `bin/quint` for an npx shim): //! //! ```text -//! PATH="$PWD/bin:$PATH" cargo test --test mbt +//! PATH="$PWD/bin:$PATH" cargo test --locked --test mbt //! ``` use conway_utxo_quint_spike::*;