chore(ledgerr-mcp): retire orphaned actor/gate channel dispatch system - #164
Merged
Conversation
…drift blocks Once #162's ledger_ops.rs fix unblocks compilation, `just check-drift` hits a second, previously-hidden failure: it calls `cargo run -p xtask-mcpb -- generate-ts-types` and `generate-py-types`, neither of which exist in xtask-mcpb anymore (only `generate-type-tables` does), and their target files (ui/docs/src/iso/generated-types.ts/.py) don't exist in the tree either. main's CI has never reached this step because it always died earlier on the conflict-marker compile error, so this drifted unnoticed. Removes the two dead blocks. Confirmed via `git log -S` on xtask/src/main.rs that these subcommands are not present, and the doc comment above check-drift doesn't reference them either. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
Comment on lines
+24
to
+38
| pub fn from_str(s: &str) -> Option<Self> { | ||
| match s.to_lowercase().as_str() { | ||
| "bitcoin" | "btc" => Some(Self::Bitcoin), | ||
| "ethereum" | "eth" => Some(Self::Ethereum), | ||
| "solana" | "sol" => Some(Self::Solana), | ||
| "cardano" | "ada" => Some(Self::Cardano), | ||
| "polkadot" | "dot" => Some(Self::Polkadot), | ||
| "avalanche" | "avax" => Some(Self::Avalanche), | ||
| "polygon" | "matic" => Some(Self::Polygon), | ||
| "arbitrum" | "arb" => Some(Self::Arbitrum), | ||
| "optimism" | "op" => Some(Self::Optimism), | ||
| "bsc" | "bnb" => Some(Self::Bsc), | ||
| other => Some(Self::Other(other.to_string())), | ||
| } | ||
| } |
Comment on lines
+24
to
+38
| pub fn from_str(s: &str) -> Option<Self> { | ||
| match s.to_lowercase().as_str() { | ||
| "bitcoin" | "btc" => Some(Self::Bitcoin), | ||
| "ethereum" | "eth" => Some(Self::Ethereum), | ||
| "solana" | "sol" => Some(Self::Solana), | ||
| "cardano" | "ada" => Some(Self::Cardano), | ||
| "polkadot" | "dot" => Some(Self::Polkadot), | ||
| "avalanche" | "avax" => Some(Self::Avalanche), | ||
| "polygon" | "matic" => Some(Self::Polygon), | ||
| "arbitrum" | "arb" => Some(Self::Arbitrum), | ||
| "optimism" | "op" => Some(Self::Optimism), | ||
| "bsc" | "bnb" => Some(Self::Bsc), | ||
| other => Some(Self::Other(other.to_string())), | ||
| } | ||
| } |
Comment on lines
+67
to
+78
| pub fn from_str(s: &str) -> Option<Self> { | ||
| match s.to_lowercase().as_str() { | ||
| "fifo" => Some(Self::Fifo), | ||
| "lifo" => Some(Self::Lifo), | ||
| "hifo" => Some(Self::Hifo), | ||
| "acb" => Some(Self::Acb), | ||
| "specific_id" | "specific_identification" => { | ||
| Some(Self::SpecificIdentification { lot_refs: vec![] }) | ||
| } | ||
| _ => None, | ||
| } | ||
| } |
Comment on lines
+67
to
+78
| pub fn from_str(s: &str) -> Option<Self> { | ||
| match s.to_lowercase().as_str() { | ||
| "fifo" => Some(Self::Fifo), | ||
| "lifo" => Some(Self::Lifo), | ||
| "hifo" => Some(Self::Hifo), | ||
| "acb" => Some(Self::Acb), | ||
| "specific_id" | "specific_identification" => { | ||
| Some(Self::SpecificIdentification { lot_refs: vec![] }) | ||
| } | ||
| _ => None, | ||
| } | ||
| } |
Comment on lines
+98
to
+103
| pub fn from_str(s: &str) -> Self { | ||
| match s.to_lowercase().as_str() { | ||
| "us" => Self::Us, | ||
| _ => Self::Au, | ||
| } | ||
| } |
Comment on lines
+98
to
+103
| pub fn from_str(s: &str) -> Self { | ||
| match s.to_lowercase().as_str() { | ||
| "us" => Self::Us, | ||
| _ => Self::Au, | ||
| } | ||
| } |
Comment on lines
+124
to
+133
| pub fn from_str(s: &str) -> Self { | ||
| match s.to_lowercase().as_str() { | ||
| "buy" => Self::Buy, | ||
| "staking" => Self::Staking, | ||
| "airdrop" => Self::Airdrop, | ||
| "spend" => Self::Spend, | ||
| "transfer" => Self::Transfer, | ||
| _ => Self::Sell, | ||
| } | ||
| } |
Comment on lines
+124
to
+133
| pub fn from_str(s: &str) -> Self { | ||
| match s.to_lowercase().as_str() { | ||
| "buy" => Self::Buy, | ||
| "staking" => Self::Staking, | ||
| "airdrop" => Self::Airdrop, | ||
| "spend" => Self::Spend, | ||
| "transfer" => Self::Transfer, | ||
| _ => Self::Sell, | ||
| } | ||
| } |
| )> = OnceLock::new(); | ||
| PAIR.get_or_init(build_service).0 | ||
| static SERVICE: OnceLock<&'static ledgerr_mcp::TurboLedgerService> = OnceLock::new(); | ||
| *SERVICE.get_or_init(build_service) |
| )> = OnceLock::new(); | ||
| PAIR.get_or_init(build_service).0 | ||
| static SERVICE: OnceLock<&'static ledgerr_mcp::TurboLedgerService> = OnceLock::new(); | ||
| *SERVICE.get_or_init(build_service) |
…12 tools) Third latent bug exposed by #162's compile fix: DOC-01 hardcoded the top-level tool catalog at 10 tools, but BUILTIN_TOOL_NAMES in mcp_adapter.rs has had 12 since ledgerr_schema/ledgerr_manifest were added — the test was never updated because main's CI never got past the ledger_ops.rs conflict-marker compile error to run it. Confirmed via crates/ledgerr-mcp/src/contract.rs: SCHEMA_TOOL = "ledgerr_schema", MANIFEST_TOOL = "ledgerr_manifest". cargo test -p ledgerr-mcp --test mcp_adapter_contract: 4/4 pass. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…m (gh#119)
actor.rs/gate.rs implemented a channel-based ServiceHandle/GateMessage
dispatch alternative to mcp_adapter.rs's direct &TurboLedgerService
calls, with its own passing unit tests — but nothing ever routed
through it. The only call site was build_service() in
ledgerr-mcp-server.rs, which spawned an actor, discarded its handle
immediately, and separately constructed and leaked a second raw
TurboLedgerService instance that all 28 mcp_adapter handlers actually
used. The doc comment atop mcp_adapter.rs claimed it was legacy and
"new code should route through actor::ServiceHandle instead," which
was aspirational, not reality.
Decision (operator sign-off, gh#119): retire rather than finish wiring
it in — mcp_adapter's direct dispatch already works, and migrating 28
handlers onto channel dispatch carries real regression risk (error
semantics, deadlocks) that would need its own TDD-per-handler plan.
- delete crates/ledgerr-mcp/src/{actor,gate}.rs and their mod decls
- remove TurboLedgerService::spawn_actor
- simplify build_service()/global_raw_service() to construct one
service instance instead of two
- correct mcp_adapter.rs's stale doc comment
- drop the now-unused crossbeam dependency
cargo check -p ledgerr-mcp --all-targets --all-features: clean.
cargo test -p ledgerr-mcp --all-features: 52/53 pass; the one failure
(doc_01_mcp_boundary_tool_catalog_exposes_reduced_top_level_surface,
asserts tool count == 10 but sees 12) is pre-existing and reproduces
identically on the unmodified base commit — unrelated to this change.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…test Tool catalog grew from 10 to 12 (schema/manifest tools added); this e2e test's tools/list assertion was never updated to match, same class of drift as the mcp_adapter_contract fix in 511fd9b.
elasticdotventures
force-pushed
the
fix/119-retire-actor-gate
branch
from
August 7, 2026 08:38
baf8e68 to
5c053fc
Compare
…st invariant xtask/src/viz_manifest.rs only registered 20 of the 28 existing `impl HasVisualization` types in ledger_core::iso_objects (missing MetaCtx, Disposition, AuRdActivity, AuRdOffset, QreActivity, UsRdcCredit, CryptoTx, CryptoWallet). The checked-in ui/docs/public/viz-manifest.json stub had never been regenerated and was still the empty placeholder from before this feature existed. pipe_viz_manifest_entry_count_is_32 asserted a count of 32 and the presence of "Classification" / "GovernanceState<Closed>" entries — neither type exists anywhere in the codebase, so this invariant was unreachable. Renamed to pipe_viz_manifest_entry_count_matches_registered_types, asserting the real count (28) and representative entries that actually exist. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr
invoice_required_pass_iff_arithmetic_holds was the only proof in this crate using f64 with more than one magnitude-unbounded symbolic operand (subtotal/gst were only constrained by is_finite()). CBMC's bit-precise floating-point theory scales very poorly across multiple interacting unbounded doubles, which lines up with this being the one CI job that has repeatedly run 3-6+ hours before the runner loses communication with the GitHub Actions server (see recent Kani Proofs run history on this branch and #162). Bounding subtotal/gst to the same practical amount range already used for total doesn't weaken the proof: solver.validate() and the test's arith_ok both compute the identical (total - subtotal - gst).abs() < 0.01 formula, so the assertion is an unconditional tautology regardless of the bound — this only shrinks the search space CBMC has to explore. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr
elasticdotventures
pushed a commit
that referenced
this pull request
Aug 7, 2026
… drift/push guardrails Local investigation (cargo kani installed + run directly, bypassing the 5-6h blind CI round trip) found invoice_required_pass_iff_arithmetic_holds was the actual cause of every "Kani model checking" CI failure on #164/#165. The property is a syntactic tautology (solver.validate() and the test compute the identical (total - subtotal - gst).abs() < 0.01 formula), but CBMC's default CaDiCaL bit-blasting solver can't discharge the auto-generated NaN safety-checks for three interacting f64 operands in bounded time. Native SMT solvers (Z3, Bitwuzla) solve the same harness in ~0.1s but the CBMC/kani-driver integration reports those checks as ERROR rather than SUCCESS — not a genuine pass, so not a safe substitute. Downgraded to concrete/edge-case #[test]s (un-gated from #[cfg(kani)] so they run under plain `cargo test` on every push); the other 4 kani-proofs harnesses (all f32) remain full symbolic proofs and verify in seconds. Also closes two other gaps surfaced this session: - check-drift never covered ui/docs/public/viz-manifest.json, the exact artifact that silently rotted for six weeks. Added it alongside the existing bindings.ts/mcp-capability-contract.md checks, in CI too. - A prior session claimed PRs #164/#165 were "pushed" when they weren't (verified after the fact via manual git fetch/rev-parse). Added `just verify-pushed` so that's a one-line check instead of trusting a push command's exit code. - Added `just kani-setup`/`just kani-check` so local Kani iteration (cargo install kani-verifier && cargo kani setup) doesn't have to be rediscovered next time. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr
… drift/push guardrails Local investigation (cargo kani installed + run directly, bypassing the 5-6h blind CI round trip) found invoice_required_pass_iff_arithmetic_holds was the actual cause of every "Kani model checking" CI failure on #164/#165. The property is a syntactic tautology (solver.validate() and the test compute the identical (total - subtotal - gst).abs() < 0.01 formula), but CBMC's default CaDiCaL bit-blasting solver can't discharge the auto-generated NaN safety-checks for three interacting f64 operands in bounded time. Native SMT solvers (Z3, Bitwuzla) solve the same harness in ~0.1s but the CBMC/kani-driver integration reports those checks as ERROR rather than SUCCESS — not a genuine pass, so not a safe substitute. Downgraded to concrete/edge-case #[test]s (un-gated from #[cfg(kani)] so they run under plain `cargo test` on every push); the other 4 kani-proofs harnesses (all f32) remain full symbolic proofs and verify in seconds. Also closes two other gaps surfaced this session: - check-drift never covered ui/docs/public/viz-manifest.json, the exact artifact that silently rotted for six weeks. Added it alongside the existing bindings.ts/mcp-capability-contract.md checks, in CI too. - A prior session claimed PRs #164/#165 were "pushed" when they weren't (verified after the fact via manual git fetch/rev-parse). Added `just verify-pushed` so that's a one-line check instead of trusting a push command's exit code. - Added `just kani-setup`/`just kani-check` so local Kani iteration (cargo install kani-verifier && cargo kani setup) doesn't have to be rediscovered next time. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr
Ran the full remaining kani-proofs suite locally (cargo kani, no --harness
filter) after the invoice_arithmetic downgrade and confirmed the other four
harnesses (vendor_constraints, z3_result x3, meta_ctx) genuinely verify in
under a second each. commit_gate_is_total was the one still hanging — and
was almost certainly the actual root cause of every historical CI timeout on
this workflow (it's the first harness Kani reaches alphabetically, so it
would block before invoice_arithmetic was ever reached).
evaluate_commit_gate()'s PendingOperator branch builds `reason` via
format!("... {:.2} ...", ...); CBMC can't bound the data-dependent loops in
Rust's float formatting internals (flt2dec::round_up), and switching to
unprecision-specified Display just traded that for an equally unbounded
Unicode table lookup (core::unicode::unicode_data::skip_search) — confirmed
locally, not guessed. This is a known general Kani limitation: format!/
Display in code reachable from a proof harness defeats automatic unwinding.
The proof's actual assertion — that the return value matches one of
CommitGate's three variants — is also a tautology of Rust's type system
(any CommitGate trivially matches its own variants), and the harness's use
of new_for_kani (always empty issues) meant the Blocked variant was never
even reachable from it. Downgraded to four concrete tests covering all three
real branches, including Blocked, which the original proof never exercised.
Remaining kani-proofs suite (4 harnesses) verified clean: `cargo kani` ->
"Complete - 5 successfully verified harnesses, 0 failures, 5 total" in ~2s
(5 because z3_result contributes 3 harnesses from one file).
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr
…ed proofs The concrete edge-case tests added when invoice_arithmetic and commit_gate were downgraded from symbolic Kani proofs run in milliseconds and only cover a handful of hand-picked cases — real correctness coverage, but not the breadth a formal proof was providing. Adds a second, #[ignore]'d tier per module: - invoice_arithmetic: dense (total, subtotal) grid in $0.01 steps up to $2,000, x6 representative gst deltas per pair — 50.4M concrete checks. - commit_gate: every confidence value on a 5,000,001-step grid across [0.0, 1.0], checked both with and without an unrecoverable issue present (10M evaluations) — this concretely exercises the format!() call in the PendingOperator branch millions of times, the exact workload that defeated Kani's symbolic unwinding, just run natively instead of symbolically. Both run in ~6.5s combined (measured) and are excluded from the default fast `cargo test` suite so normal iteration stays fast; run explicitly via the new `just exhaustive-check` recipe before a release or when auditing either invariant. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr
elasticdotventures
added a commit
that referenced
this pull request
Aug 9, 2026
* fix(ledger-core): repair committed conflict fragments * fix(justfile): remove dead generate-ts-types/generate-py-types check-drift blocks Once #162's ledger_ops.rs fix unblocks compilation, `just check-drift` hits a second, previously-hidden failure: it calls `cargo run -p xtask-mcpb -- generate-ts-types` and `generate-py-types`, neither of which exist in xtask-mcpb anymore (only `generate-type-tables` does), and their target files (ui/docs/src/iso/generated-types.ts/.py) don't exist in the tree either. main's CI has never reached this step because it always died earlier on the conflict-marker compile error, so this drifted unnoticed. Removes the two dead blocks. Confirmed via `git log -S` on xtask/src/main.rs that these subcommands are not present, and the doc comment above check-drift doesn't reference them either. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(ledgerr-mcp): update stale MCP tool catalog contract test (10 -> 12 tools) Third latent bug exposed by #162's compile fix: DOC-01 hardcoded the top-level tool catalog at 10 tools, but BUILTIN_TOOL_NAMES in mcp_adapter.rs has had 12 since ledgerr_schema/ledgerr_manifest were added — the test was never updated because main's CI never got past the ledger_ops.rs conflict-marker compile error to run it. Confirmed via crates/ledgerr-mcp/src/contract.rs: SCHEMA_TOOL = "ledgerr_schema", MANIFEST_TOOL = "ledgerr_manifest". cargo test -p ledgerr-mcp --test mcp_adapter_contract: 4/4 pass. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * docs: add implementation plan for gh#118 Phase A (settings unification) Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * feat(ledgrrr-settings): scaffold new crate, move settings_backend * fix(ledgrrr-settings): remove fabricated stub modules, scope lib.rs to Task 1's actual deliverable (backend only) Removes five stub files that Task 1's implementer created to satisfy the given lib.rs template (model_provider.rs, notification.rs, path.rs, schema.rs, store.rs). These stubs were placeholders for real modules that Tasks 2–4 will deliver, and their presence forces unnecessary overwrite/conflict resolution in those tasks. lib.rs is now scoped to only Task 1's actual deliverable: the backend module and its public API, with no synthetic re-exports. Later tasks (2, 3, 4) will add their own modules incrementally as they land their real implementations. Verification: - cargo check -p ledgrrr-settings --all-targets: PASS - cargo test -p ledgrrr-settings: 4/4 backend tests pass - cargo check --workspace: PASS Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * refactor(ledgerr-host): move NotificationBackend/Status/TestResult to ledgrrr-settings Move three notification types from ledgerr-host to the new ledgrrr-settings crate: - NotificationBackend enum - NotificationStatus enum - NotificationTestResult struct These types are now re-exported from ledgrrr_settings in both ledgerr-host and ledgrrr-settings for downstream consumption. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * refactor(ledgerr-host): move ModelProviderLabel to ledgrrr-settings Move ModelProviderLabel enum and ProviderReadiness to ledgrrr-settings/model_provider. Implement display_name() and description() as inherent methods. Methods requiring ledgerr-host types (chat_settings, readiness) are provided via ModelProviderExt trait to avoid circular dependencies. - Creates crates/ledgrrr-settings/src/model_provider.rs with ModelProviderLabel and ProviderReadiness enums plus basic inherent methods - Updates internal_openai.rs to re-export types and implement extension trait - Maintains API compatibility: trait is automatically in scope via wildcard imports Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * refactor(ledgerr-host): move AppSettings/SettingsStore/default_settings_path to ledgrrr-settings * feat(package): package ledgrrr-mcp desktop controller as .mcpb for Claude Desktop (#120) * feat(desktop-agent): supersede stub with full PRD-10 §3.1 ledgrrr-mcp controller Replaces the two-tool desktop_status/desktop_ping stub from #120 with the complete PRD-10 desktop controller: two bins (ledgrrr-mcp, ledgrrr-service) and 9 modules (contract, status, render, simulate, playbook, office_artifact, service_control, install_plan, state) implementing all eleven ledgrrr_* tools with real state (b00t CLI, service liveness via sysinfo, tray binary presence), deterministic Mermaid/JSON/SVG rendering, a governance-correct non-LLM simulation engine, and versioned local Office artifact export. Packaging script/Justfile recipe/README updated to match: binary is ledgrrr-mcp (not ledgerr-desktop-agent), bundle is ledgrrr-claude.mcpb per PRD-10 §3.1 naming rather than the placeholder name from #120. 18/18 tests pass; clippy clean; packaging script verified end-to-end (builds the release binary, assembles the bundle, and the packaged binary answers a real MCP initialize handshake over stdio). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * docs(desktop-agent): add PRD-11 spec + book chapter, renumbered from colliding PRD-10 task/31-windows-packaging wrote its desktop-agent requirements doc as PRD-10.md, but main's PRD-10.md is a different, unrelated document ("Financial Pipeline — Ingestion, Workbook Write, and AGT Governance Wiring", already referenced throughout crates/ledgerr-mcp/src/actor.rs and gate.rs). Renumbered the desktop-agent spec to PRD-11 and updated every reference inside crates/ledgerr-desktop-agent/, scripts/, the Justfile, and README.md accordingly — the ledgerr-mcp governance PRD-10 references were left untouched. Adds book/src/desktop-agent-office-playbook.md (wired into SUMMARY.md, mcp-surface.md, and visualize.md) and the README threads (MECE tables, capability snapshot, Future Ambitions section) from the original docs commit, updated to reflect what's actually implemented now (MCPB packaging works) rather than the "missing" status written before it existed. 18/18 tests pass; clippy clean; packaging script re-verified after the rename (builds, bundles, and the packaged binary still answers a real MCP initialize handshake). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(ledgerr-desktop-agent): TRAY_CANDIDATES named a binary (ledgerr-tauri) that doesn't exist Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * feat(ledgerr-desktop-agent): add settings HTTP server (GET/POST /settings) * feat(ledgerr-desktop-agent): serve settings HTTP endpoint from ledgrrr-service's main loop * feat(host-tauri): settings now served by ledgrrr-service over HTTP, not a local SettingsStore * feat(host-tray): settings now served by ledgrrr-service over HTTP, shared SettingsClient with host-tauri * docs: mark gh#118 Phase A (settings unification) complete in the integration roadmap * fix: address final whole-branch review findings (dead code, Default impl, doc gap) * fix(ledgerr-host): resolve clippy violations in internal_openai.rs Move resolve_chat_settings above the #[cfg(test)] mod tests block (clippy::items_after_test_module) and drop the unnecessary ::default() call on the Phi4LocalFallbackBackend unit struct (clippy::default_constructed_unit_structs). * fix(ledgerr-mcp): update stale tool-count assertion in mcp_stdio_e2e test Same drift as fix/119-retire-actor-gate's 5c053fc: tool catalog grew from 10 to 12 (schema/manifest tools), this e2e test's tools/list assertion wasn't updated. Inherited here because this branch is based on #162's tip, which predates that fix landing on the shared branch. * fix(viz-manifest): register all 28 HasVisualization impls, correct test invariant xtask/src/viz_manifest.rs only registered 20 of the 28 existing `impl HasVisualization` types in ledger_core::iso_objects (missing MetaCtx, Disposition, AuRdActivity, AuRdOffset, QreActivity, UsRdcCredit, CryptoTx, CryptoWallet). The checked-in ui/docs/public/viz-manifest.json stub had never been regenerated and was still the empty placeholder from before this feature existed. pipe_viz_manifest_entry_count_is_32 asserted a count of 32 and the presence of "Classification" / "GovernanceState<Closed>" entries — neither type exists anywhere in the codebase, so this invariant was unreachable. Renamed to pipe_viz_manifest_entry_count_matches_registered_types, asserting the real count (28) and representative entries that actually exist. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr * fix(kani-proofs): bound subtotal/gst magnitude to curb f64 SMT blowup invoice_required_pass_iff_arithmetic_holds was the only proof in this crate using f64 with more than one magnitude-unbounded symbolic operand (subtotal/gst were only constrained by is_finite()). CBMC's bit-precise floating-point theory scales very poorly across multiple interacting unbounded doubles, which lines up with this being the one CI job that has repeatedly run 3-6+ hours before the runner loses communication with the GitHub Actions server (see recent Kani Proofs run history on this branch and #162). Bounding subtotal/gst to the same practical amount range already used for total doesn't weaken the proof: solver.validate() and the test's arith_ok both compute the identical (total - subtotal - gst).abs() < 0.01 formula, so the assertion is an unconditional tautology regardless of the bound — this only shrinks the search space CBMC has to explore. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr * fix(kani-proofs): downgrade invoice_arithmetic to concrete tests, add drift/push guardrails Local investigation (cargo kani installed + run directly, bypassing the 5-6h blind CI round trip) found invoice_required_pass_iff_arithmetic_holds was the actual cause of every "Kani model checking" CI failure on #164/#165. The property is a syntactic tautology (solver.validate() and the test compute the identical (total - subtotal - gst).abs() < 0.01 formula), but CBMC's default CaDiCaL bit-blasting solver can't discharge the auto-generated NaN safety-checks for three interacting f64 operands in bounded time. Native SMT solvers (Z3, Bitwuzla) solve the same harness in ~0.1s but the CBMC/kani-driver integration reports those checks as ERROR rather than SUCCESS — not a genuine pass, so not a safe substitute. Downgraded to concrete/edge-case #[test]s (un-gated from #[cfg(kani)] so they run under plain `cargo test` on every push); the other 4 kani-proofs harnesses (all f32) remain full symbolic proofs and verify in seconds. Also closes two other gaps surfaced this session: - check-drift never covered ui/docs/public/viz-manifest.json, the exact artifact that silently rotted for six weeks. Added it alongside the existing bindings.ts/mcp-capability-contract.md checks, in CI too. - A prior session claimed PRs #164/#165 were "pushed" when they weren't (verified after the fact via manual git fetch/rev-parse). Added `just verify-pushed` so that's a one-line check instead of trusting a push command's exit code. - Added `just kani-setup`/`just kani-check` so local Kani iteration (cargo install kani-verifier && cargo kani setup) doesn't have to be rediscovered next time. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr * fix(kani-proofs): downgrade commit_gate_is_total — the actual CI blocker Ran the full remaining kani-proofs suite locally (cargo kani, no --harness filter) after the invoice_arithmetic downgrade and confirmed the other four harnesses (vendor_constraints, z3_result x3, meta_ctx) genuinely verify in under a second each. commit_gate_is_total was the one still hanging — and was almost certainly the actual root cause of every historical CI timeout on this workflow (it's the first harness Kani reaches alphabetically, so it would block before invoice_arithmetic was ever reached). evaluate_commit_gate()'s PendingOperator branch builds `reason` via format!("... {:.2} ...", ...); CBMC can't bound the data-dependent loops in Rust's float formatting internals (flt2dec::round_up), and switching to unprecision-specified Display just traded that for an equally unbounded Unicode table lookup (core::unicode::unicode_data::skip_search) — confirmed locally, not guessed. This is a known general Kani limitation: format!/ Display in code reachable from a proof harness defeats automatic unwinding. The proof's actual assertion — that the return value matches one of CommitGate's three variants — is also a tautology of Rust's type system (any CommitGate trivially matches its own variants), and the harness's use of new_for_kani (always empty issues) meant the Blocked variant was never even reachable from it. Downgraded to four concrete tests covering all three real branches, including Blocked, which the original proof never exercised. Remaining kani-proofs suite (4 harnesses) verified clean: `cargo kani` -> "Complete - 5 successfully verified harnesses, 0 failures, 5 total" in ~2s (5 because z3_result contributes 3 harnesses from one file). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr * test(kani-proofs): add exhaustive/full-compliance sweeps for downgraded proofs The concrete edge-case tests added when invoice_arithmetic and commit_gate were downgraded from symbolic Kani proofs run in milliseconds and only cover a handful of hand-picked cases — real correctness coverage, but not the breadth a formal proof was providing. Adds a second, #[ignore]'d tier per module: - invoice_arithmetic: dense (total, subtotal) grid in $0.01 steps up to $2,000, x6 representative gst deltas per pair — 50.4M concrete checks. - commit_gate: every confidence value on a 5,000,001-step grid across [0.0, 1.0], checked both with and without an unrecoverable issue present (10M evaluations) — this concretely exercises the format!() call in the PendingOperator branch millions of times, the exact workload that defeated Kani's symbolic unwinding, just run natively instead of symbolically. Both run in ~6.5s combined (measured) and are excluded from the default fast `cargo test` suite so normal iteration stays fast; run explicitly via the new `just exhaustive-check` recipe before a release or when auditing either invariant. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014WXX8Nx14N3QJ8jcxmcfnr * docs: complete project research * docs: define milestone v1.3 requirements * docs: create milestone v1.3 roadmap (3 phases) * docs: complete phase 22 (release automation foundation) * fix(ledgrrr-settings): stop windows_registry::* from shadowing std::result::Result The glob import brought in windows_registry's re-exported Result<T> type alias (single generic parameter, error type hardcoded to windows_result::Error), shadowing std::result::Result used throughout this file's Result<T, SettingsBackendError> signatures. Only surfaced on a native windows-latest build; this crate has no compile coverage on non-Windows dev hosts. * fix(ledgerr-host): migrate tray/native.rs to windows-rs 0.62 API First real CI compile of this file (PR #911, windows-latest) surfaced 24 errors, all API-mismatch or plain type-system issues against windows 0.62.2 / windows-core 0.62.2 (this crate has never built here before now): - BOOL and PCWSTR moved out of the Win32::Foundation glob re-export; both now live in windows::core (windows-result::BOOL, windows-strings::PCWSTR) and need an explicit `use windows::core::{w, BOOL, PCWSTR};`. Same story for the `w!` literal macro (one bare use wasn't fully qualified). - HBITMAP -> HGDIOBJ and HMODULE -> HINSTANCE are now distinct newtypes instead of being interchangeable; added `.into()` at each DeleteObject, WNDCLASSW.hInstance, and CreateWindowExW call site. - BI_RGB is now a BI_COMPRESSION newtype, not a bare u32; use `.0`. - PostMessageW's hwnd parameter is `Option<HWND>` in 0.62; wrap in `Some`. - `WM_APP + 1` used directly as a match pattern is invalid Rust (arbitrary expressions aren't patterns) regardless of windows-rs version; extracted to a named const `WM_TRAYICON_CALLBACK` used both as the match arm and the NOTIFYICONDATAW.uCallbackMessage value. - std::sync::mpsc::Sender has no `is_closed`; dropped the probe and rely on `send` returning Err on a disconnected receiver instead, which also required changing run_tray_pump's ready_tx parameter from an owned Sender to `&Sender` so the caller can still use it after the call for error reporting (the owned param was silently moved into the call, which would have been its own separate "use of moved value" error once the missing method issue was fixed). - create_icon_from_rgba and build_tray_menu (plus its nested push_info / push_action / push_check helpers) returned Box<dyn Error> while their caller's `?` needs Box<dyn Error + Send + Sync>; aligned all of their return types to match rather than map_err at each call site. Verified every API shape against the locally cached windows-core-0.62.2 and windows-0.62.2 crate sources (registry checkout) rather than against memory of older windows-rs majors, per the task's caution that this file has no prior working revision to trust. * fix(ledgerr-host): wrap AppendMenuW calls in unsafe blocks Nested fn items (push_info/push_action/push_check) don't inherit unsafety from the enclosing unsafe fn build_tray_menu -- each needs its own explicit unsafe block around the AppendMenuW call. * fix(holon-viz): derive specta::Type on Cytoscape* structs specta::specta-annotated Tauri commands returning Result<CytoscapeGraph, String> require CytoscapeGraph (and its field types) to implement specta's Type trait via the blanket FunctionResult impl. Add the derive to CytoscapeNodeData, CytoscapeNode, CytoscapeEdgeData, CytoscapeEdge, and CytoscapeGraph, and add specta as a holon-viz dependency (pinned to the same =2.0.0-rc.25 version ledgerr-host already uses, with the derive feature enabled). Fixes E0277 FunctionResult<_> not satisfied at commands.rs:541 and :649. --------- Co-authored-by: brianh <brianh@promptexecution.com> Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes #119.
actor.rs/gate.rsimplemented a channel-basedServiceHandle/GateMessagedispatch alternative tomcp_adapter.rs's direct&TurboLedgerServicecalls, with its own passing unit tests — but nothing ever routed through it. The only call site wasbuild_service()inledgerr-mcp-server.rs, which spawned an actor, discarded its handle immediately, and separately constructed and leaked a second rawTurboLedgerServiceinstance that all 28mcp_adapterhandlers actually used. The doc comment atopmcp_adapter.rsclaimed it was legacy and "new code should route throughactor::ServiceHandleinstead" — aspirational, not reality.Decision (operator sign-off, per #119): retire rather than finish wiring it in.
mcp_adapter's direct dispatch already works; migrating 28 handlers onto channel dispatch carries real regression risk (error semantics, deadlocks) that would need its own TDD-per-handler plan, not a rush job.Changes
crates/ledgerr-mcp/src/{actor,gate}.rsand theirmoddeclarationsTurboLedgerService::spawn_actorbuild_service()/global_raw_service()to construct one service instance instead of twomcp_adapter.rs's stale doc commentcrossbeamdependencyThis branch is stacked on
agent/repair-ledger-ops-conflict(#162) becausemain'sledger-corecurrently fails to compile (committed conflict-marker fragments inledger_ops.rs) — there's no other base where this change can be verified to actually build. Should not merge before #162.Validation
cargo check -p ledgerr-mcp --all-targets --all-features: cleancargo test -p ledgerr-mcp --all-features: 52/53 pass. The one failure (doc_01_mcp_boundary_tool_catalog_exposes_reduced_top_level_surface, asserts tool count == 10 but sees 12) is pre-existing and reproduces identically on the unmodified base commit — confirmed unrelated to this change before committing.🤖 Generated with Claude Code