feat(abi): Tier-2 Idris bindings + retire legacy Foreign + close L10 transitive cycle - #52
Merged
Merged
Conversation
…L10 transitive cycle Three closures from the standards#124 Phase-5 follow-up: A. **VclTotal.ABI.Foreign → VclTotal.Legacy.Foreign.** The legacy `libvqlut` pipeline binding (Zig-side `achieved_level` assertion, no Idris certificate) is moved to `src/interface/legacy/` with a deprecation banner pointing at Tier-1 (recompute-PCC over wasm32) and Tier-2 (Ed25519 signed attestation). The stale corpus symlink `corpus/VclTotal/ABI/Foreign.idr` is removed (Foreign was never in the proof corpus). New consumers should target the honest paths. B. **NEW `VclTotal.ABI.Tier2` at `src/interface/abi/Tier2.idr`.** Idris bindings to the honest C ABI `vclut_verify_wire` (`ffi/zig/src/lib.zig` → `src/interface/attest::vclut_rs_verify`). Exposes `verifyWire : List Bits8 → List Bits8 → List Bits8 → IO Tier2Verdict` with a `Verified SafetyLevel (List Bits8) | Rejected String` typed sum and fail-closed contract at every layer (seed width check, alloc failure → Rejected, negative `c_int` → Rejected, out-of-range level → defensive Rejected). The 65-byte attestation `[level:1][sig:64]` is returned on success. C. **L10 transitive ENTAILS cycle decider** (`src/core/Decide.idr`). `hasCircularEntails` (direct A⊨B ∧ B⊨A only) is supplemented by `hasTransitiveCycle`, which computes the transitive closure of the ENTAILS edge list to a `length pairs` fuel bound (finite, total) and reports any (x,x). `epiNoCycle` now uses the transitive form. Closes the L10 hole that the direct check missed. Verification: - `idris2 --build verification/proofs/vclut-core.ipkg` -> 12/12 modules build clean from a fresh `build/`. Only pre-existing benign `n`-shadowing warnings in `Layout.idr`. - `VclTotal.ABI.Tier2` typechecks cleanly when wired through the corpus tree (not added to the manifest because it is FFI plumbing, not a proof; same policy as `ABI.Foreign` was). - VERIFICATION-STANCE.adoc updated to record L10 closure (Phase 4b/5), Foreign retirement (no longer an OWED), and Tier2 as the consumer-facing replacement. - ABI-FFI-README.adoc directory diagrams updated. Trust model deltas: - Tier-1 (recompute) remains the strongest tier; Tier-2 is the honest C-ABI fallback; legacy is documented as deprecated. - No new axioms; no proof-escape symbols (no believe_me/postulate/assert_/sorry/idris_crash) in any proof-corpus module. Refs hyperpolymath/standards#124 (Phase 5 follow-up). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
marked this pull request as ready for review
June 5, 2026 13:43
hyperpolymath
enabled auto-merge (squash)
June 5, 2026 13:43
hyperpolymath
pushed a commit
that referenced
this pull request
Jun 11, 2026
…ifications bufferToList now recurses structurally on a remaining-byte Nat fuel instead of asserting totality on an increasing Int index. Semantics unchanged (n <= 0 yields [], bytes read [0, n) in order); the totality checker accepts it directly, restoring the proof-corpus zero proof-escape contract that #52's merge gate promised. audits/assail-classifications.a2ml records the audited FFI residuals from a fresh panic-attack 2.5.5 scan: the documented unsafe blocks in recompute-wasm and attest (both files carry in-file UNSAFE POLICY sections and deny(clippy::undocumented_unsafe_blocks)) and the Zig C-ABI bridge cast. The assert_total finding is fixed, not classified. vcl-ut also gains scan coverage for the first time: it had NO entry in verisimdb-data/scans at all (coverage gap fixed estate-wide by hypatia's new estate-rescan workflow).
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
1 participant
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.
Reconciles the parked
claude/abi-tier2-and-l10-trans-cyclebranch intomain(branch-reconciliation pass, owner-approved). Unmerged since 2026-06-03.Substantive proof/ABI work:
src/interface/abi/Tier2.idr(+209) — Tier-2 Idris bindingssrc/core/Decide.idr(+79) — closes the L10 transitive cycleabi/Foreign.idr→legacy/Foreign.idrverification/proofs/VERIFICATION-STANCE.adoc(+121)Merge gate: the Idris2 proof corpus (
proof-corpus.yml) must stay green —%default total, zero proof-escape — before this lands. Draft until CI confirms. Likely needs a rebase onto currentmain(post #48/#49/#50, incl. the licence normalisation).https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME
Generated by Claude Code