proof: discharge proof-obligation map Tiers 0–3 (#84)#106
Merged
Conversation
hyperpolymath
marked this pull request as ready for review
June 2, 2026 11:17
hyperpolymath
enabled auto-merge
June 2, 2026 11:22
hyperpolymath
changed the title
Convert the 6 operational unwrap/expect sites to error propagation / non-panicking handling, and lock it in with #![cfg_attr(not(test), deny(clippy::unwrap_used, clippy::expect_used))] on every crate so regressions fail clippy. - esn: create_recurrent_weights/create_input_weights -> Result, propagated in new() - lsm: create_recurrent_weights/create_input_weights -> Result, propagated in new() - sensors: reset() reconstructs the window without unwrap (args provably valid) - bridge/llm/neurophone-core/claude-client: guard added (already panic-free) clippy --workspace clean (guard active); cargo test --workspace all green. Also records the standing work-ordering rule (full-lowest-tier-first) in methodology.a2ml. https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
Property tests over extreme finite inputs across long runs assert no NaN/Inf propagates through the numeric kernels: - esn::step (reservoir update) - lsm::step (spiking dynamics) - sensors IIR low/high-pass filter cascade Add proptest to lsm dev-dependencies (others already had it). https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
- Fix create_recurrent_weights: scale by the true spectral radius (power iteration) instead of the infinity-norm (max abs row sum) — same flaw fixed in esn (1.1). Drops now-unused Axis import. - Add verification getters: membrane_potentials(), lif_params(), history_window_ms(), max_spike_history_len(). - proptest_bounds: across long runs of bounded input, every membrane potential stays finite and <= threshold (spike resets within the step), and per-neuron spike history stays within the window/refractory bound. clippy -p lsm clean; cargo test -p lsm all green. https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
Encoder is a lossy summariser (no inverse), so soundness = totality + determinism + well-formed bounded outputs: - total: defined on all finite inputs incl. empty/mismatched lengths, no panic - deterministic: identical input sequences -> identical NeuralContext (incl. the history-dependent urgency term) - well-formed: salience/urgency in [0,1] and finite; active counts <= lengths; description never empty clippy -p bridge clean; cargo test -p bridge green. https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
…91) Encode the lifecycle in the type: NeuroSymbolicSystem<S> with phase markers Created -> Active -> Down. new() yields Created; initialize() consumes it and returns Active; process_sensor_event/query exist ONLY on Active; shutdown() consumes Active and returns Down (terminal). Inspectors (get_state, uptime_ms, query_count, config) available in every phase. Illegal lifecycle use is now a COMPILE error, not a runtime check: - query/process before initialize -> won't compile - use after shutdown -> won't compile (shutdown consumes self) - restart after shutdown / double shutdown -> impossible by construction Removed the runtime is_active guard in process_sensor_event (now type-enforced). Migrated all tests/benches to the consuming flow; removed tests asserting the now-impossible behaviours (their guarantee is compile-time). Matches the terminal-shutdown TLA+ spec in proofs/tla/Lifecycle.tla. cargo test -p neurophone-core green (53 tests); clippy --all-targets clean. https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
Data-race freedom is compiler-given (no unsafe; shared state only via Mutex) and deadlock-freedom follows from a single lock (no ordering, no condvars). Add a heavy-contention test (8 threads x 250 queries) asserting query_count == 2000 — proving the mutex serialises each read-modify-write with no lost updates; completion also demonstrates no deadlock. (loom omitted: a single-lock design has no lock-free interleavings to model.) https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
#93) - proofs/affine/README.adoc: record obligation 2.3 — Rust ownership/Drop already gives acquire-release-exactly-once for owned handle types (no unsafe), and the lifecycle typestate (2.1) extends move-once to the orchestrator; the stronger linear (must-use) guarantee is deferred to AffineScript as a design spec per the Tier-2 decision. - Align two new test files' SPDX headers to the branch canonical (PMPL) to keep Licence-consistency green (not a licence change — matching new files). https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
…#94,#95) 3.1 data-egress / privacy: - Extract build_system(): neural (sensor-derived) context is placed on the wire ONLY when include_neural_context is true. - egress_request_body_has_only_allowed_fields: serialised request carries only declared fields (api key is a header, never the body; no device/sensor fields). - neural_context_not_sent_when_disabled. 3.2 bounded external interaction: - backoff_delay(): saturating + capped at 60s (fixes a latent 2u64.pow overflow); retry loop is 0..=max_retries then errors, so it always terminates. - backoff_is_bounded_and_monotonic; user_content_cannot_inject_into_request_json (typed JSON serialisation escapes user content). clippy -p claude-client --all-targets clean; tests green. https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw
hyperpolymath
force-pushed
the
claude/proof-obligations
branch
from
June 2, 2026 11:36
9031677 to
1c70b7a
Compare
This was referenced Jun 2, 2026
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
… PMPL.txt (#118) ## Summary Completes the PMPL→MPL-2.0 cleanup started in #102. After #102 landed, PR #106 added 5 new property-test files with stray \`PMPL-1.0-or-later\` SPDX headers — same drift pattern. Also NOTICE still asserted PMPL governance with the OLD "MPL is just a compat shim" framing that the 2026-06-02 owner directive explicitly supersedes. ## Changes (8 files) - 5 .rs property-test files: SPDX header \`PMPL-1.0-or-later\` → \`MPL-2.0\` - \`crates/lsm/tests/proptest_numeric.rs\` - \`crates/lsm/tests/proptest_bounds.rs\` - \`crates/sensors/tests/proptest_numeric.rs\` - \`crates/esn/tests/proptest_numeric.rs\` - \`crates/bridge/tests/proptest_soundness.rs\` - \`proofs/affine/README.adoc\`: same SPDX fix - \`NOTICE\`: rewritten to plain MPL-2.0 statement (drops Palimpsest narrative + the misleading "MPL is just a compat shim" claim) - \`LICENSES/PMPL-1.0-or-later.txt\`: deleted (orphan after this commit) ## Verification \`\`\` grep -rln 'SPDX-License-Identifier:.*PMPL\|MPL.*or-later' . → zero matches outside .git/ \`\`\` ## Test plan - [ ] Governance / Licence consistency green - [ ] No CI regression vs pre-PR baseline 🤖 Generated with [Claude Code](https://claude.com/claude-code) Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced Jun 2, 2026
hyperpolymath
added a commit
that referenced
this pull request
Jun 6, 2026
## Consolidation: fix the one real CI red + a stale licence badge ### `rust-ci` — the only foundational CI failure on `main` `rust-ci.yml` pinned the estate reusable at SHA `cc5a372…`, which is **stale** (the `standards` rust-ci-reusable moved). The run failed at **startup with 0 jobs** on `main` — not a Rust code failure (the workspace is green locally and via #106). Re-pinned to `@main`, matching the working `governance.yml`. Once `standards` publishes a verified SHA, this should be re-pinned (ideally by estate propagation). ### README licence badge The top badge still read **`License: PMPL-1.0`**; the repo is **MPL-2.0** (`Cargo.toml`, `LICENSE`, all SPDX headers, post-#102/#118). Corrected to MPL-2.0. The *Palimpsest philosophy* badge is intentional estate identity and left untouched. ### Context / non-goals - The two perpetual Kotlin reds are already resolved on `main` (carve-out #105 + `.hypatia-baseline.json`); `Language Policy` and `Governance` are green. - Other reds (Instant Sync, Mirror, Scorecard) are infrastructure/external-forge/token issues, out of scope here. - Other PMPL/Palimpsest *philosophy* mentions (`PALIMPSEST.adoc`, citations, governance audit) are deliberate and untouched — licence/philosophy is owner territory. Merging once CI (esp. `rust-ci`) is green. https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw --- _Generated by [Claude Code](https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 6, 2026
Two pieces of session housekeeping: 1. **`.gitignore`** — ignore `.claude/worktrees/` (the agent worktree dirs the gossamer sub-PR agents created), so they stop showing as untracked. 2. **`HANDOVER.adoc`** — a durable post-compaction handover capturing the full session state: proof tiers 0–3 merged (#106/#101), `main` state (MPL licence, android carve-out, the upstream `rust-ci`/`hypatia-scan` reds), my open PRs and recommended merge order (#129 first), the gossamer migration map (#83 → sub-issues #108–#115 → draft sub-PRs #121–#130), the blocked owner decisions, and the dispatchable prompts already drafted. No code or behaviour change. https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw --------- Co-authored-by: Claude <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
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Proof-obligation map (#84) — Tiers 0–3, batched
Full lowest-tier-first. Entire workspace:
cargo clippy --workspace --all-targetsclean,cargo test --workspaceall green.Tier 0 — foundations
unwrap/expectremoved;cfg_attr(not(test), deny(clippy::unwrap_used, expect_used))on every crate.esn::step,lsm::step, sensors IIR.deny/forbid(on main).Tier 1 — core algorithmic correctness
Tier 2 — system orchestration
Created→Active→Down, terminal shutdown); illegal transitions don't compile. Matchesproofs/tla/Lifecycle.tla.proofs/affine/); Rust ownership gives acquire-release-once today, AffineScript linear handles deferred.Tier 3 — trust boundary
powoverflow); injection-safety via typed JSON.Closes #86 #87 #89 #90 #91 #92 #94 #95 (1.1/#88 already merged via #101; 2.3/#93 remains a tracked spec).
The two Kotlin banned-language CI checks are red from
main'sandroid/app (tracked in #83), not from this PR.https://claude.ai/code/session_01Gu1JFCZHuBtBhAWPr4sMQw