fix(soundness): FFI octad ops fail loudly instead of reporting false success#179
Merged
Conversation
Add Verisimiser.ABI.Invariants, a second, deeper machine-checked theorem over the existing Octad model (distinct from the Layer-2 Octad<->Fin 8 bijection). Models the write effect of an augmentation *pipeline* as a join over a two-point lattice (ReadOnly <= Writes, Writes absorbing) and proves: - effectHomomorphism: pipelineEffect is a monoid homomorphism from list append to joinE (with joinAssoc / identity laws). - tier1PipelineReadOnly (CLOSURE): any pipeline of only Tier-1 dimensions is read-only -- isolation is preserved under composition (reuses Layer-2 tier1NeverWritesTarget). - writerContaminates (CONTAMINATION) + appendMonotone (MONOTONICITY): one target-writing step taints the whole pipeline. - decReadOnly: sound + complete decision procedure. - Positive control (readPathIsReadOnly) + negative controls (overlayNotReadOnly, decOverlayIsNo, effectsDistinct). No believe_me/postulate/assert_total/etc. Builds with zero warnings; adversarial false-proof rejected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
Prove the FFI result-code encoding is SOUND, not just structurally name/value-matched by scripts/abi-ffi-gate.py: - intToResult decoder + resultRoundTrip: resultToInt is faithful/lossless (every Result round-trips back from its C integer). - resultToIntInjective: DERIVED from the round-trip via cong + justInj (distinct ABI outcomes never collide on the wire). - Positive controls (decode 0/7/99 by Refl) and a machine-checked non-vacuity control (Ok and Error encode to distinct ints). - (c) Same injectivity for every other FFI enum encoder in Types: octadToInt, backendToInt, provenanceOpToInt, driftToInt, accessPolicyToInt (no ProofStatus/statusToInt in this repo). Genuine total proof: no believe_me/postulate/assert_total/etc. Builds clean (idris2 0.7.0, 0 warnings); false seam claims rejected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
Assemble the existing per-layer proofs into one inhabited certificate value
in Verisimiser.ABI.Capstone:
- ABISound record: one field per discharged layer
* flagship octad bijection (Layer-2 Octad.idr): octadFinInverseL/R
* compositional sidecar-isolation invariant (Layer-3 Invariants.idr):
readPathIsReadOnly on the canonical positive-control pipeline
* FFI-seam injectivity (Layer-4 FfiSeam.idr): resultToIntInjective
- abiContractDischarged : ABISound, built solely from real exported witnesses.
Typechecks iff every prior layer remains sound; a false field (e.g. claiming
the overlay pipeline is read-only) is rejected by the type checker.
Pure composition: no believe_me/postulate/assert/idris_crash. %default total,
zero build warnings.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
…ble fix); port ABI-FFI gate Python->Bash (Python is estate-banned) Resolves the standing baseline CI reds (rust-ci toolchain error, governance Language/anti-pattern, governance workflow-lint) without altering the proven ABI. The Bash gate reproduces the former Python gate's verdict verbatim (validated across all -iser repos) and catches the same drift classes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
…needed (rust-ci self-contained, ABI-FFI gate already canonical Julia)
The Zig FFI octad operations validated their arguments and then returned
.ok without doing the work — so callers were told an action succeeded when
it did not. The worst case, verisimiser_verify_provenance, returned .ok
('verified') without walking the hash chain, so a TAMPERED provenance
chain would pass as verified. record_provenance, record_version, and
enable_dimension likewise silently no-op'd.
Until the sidecar persistence is wired in (breadth, separate work), these
now fail loudly with .sidecar_unavailable rather than claim a success they
can't back (doctrine: no silent green). The argument-validation paths
(null handle, invalid enum) are unchanged.
Also: validate_manifest never called effective_backend(), so a manifest
with conflicting [database].backend and legacy target-db passed validation
and only failed later at generate time — now surfaced as a failed
'backend-unambiguous' check.
Adds Zig tests asserting the four ops do not return .ok with a valid
handle, and a Rust test for the manifest backend-conflict check.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes five soundness holes found in a focused audit — places where the FFI/validation reported success without delivering it.
The most serious:
verisimiser_verify_provenancereturned.ok("verified") without walking the hash chain, so a tampered provenance chain passed as verified.record_provenance,record_version, andenable_dimensionlikewise validated their enums and then silently no-op'd while returning.ok, so callers believed data had been recorded / a dimension enabled when nothing happened. The Idris2 ABI proofs (HashChain/Version/Octad) and the Rusttier1library are sound; the gap was the un-wired Zig FFI layer claiming success.Per doctrine ("fail loudly, seal soundly — no silent green"), these now return
.sidecar_unavailableuntil the sidecar persistence is wired in (that wiring is breadth, deferred). Argument-validation paths (null handle →.null_pointer, invalid enum →.invalid_param) are unchanged. NoResultvariant was added, so the ABI-FFI gate stays green.Also fixed:
validate_manifestnever calledeffective_backend(), so a manifest with conflicting[database].backendand legacytarget-dbpassed validation and only failed later at generate time — now surfaced up front as a failedbackend-unambiguouscheck.Changes
src/interface/ffi/src/main.zig:verify_provenance/record_provenance/record_version/enable_dimensionreturn.sidecar_unavailable(with a clear error message) instead of a false.ok.src/manifest/mod.rs:validate_manifestadds abackend-unambiguouscheck that exerciseseffective_backend().Testing
.okwith a valid handle (and returns.sidecar_unavailable). Existing null/invalid-enum tests unchanged. (zig testruns in the ABI-FFI gate.)conflicting_backend_fails_validation. Full suite green under the CI toolchain (1.96.0):cargo fmt --check,cargo clippy --all-targets -- -D warnings,cargo test --locked --all-targets(146 lib tests).RSR Quality Checklist
🤖 Generated with Claude Code
Generated by Claude Code