Repository navigation
licence: normalise to MPL-2.0 - #50
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>
Owner-directed single-file SPDX edit. Sibling proof-corpus files (Decide.idr, LayoutProofs.idr, VERIFICATION-STANCE.adoc) committed at 28aac38 under MPL-2.0; this file lagged at AGPL-3.0-or-later (and PMPL-1.0-or-later before a parallel sweep flipped it). Aligning to the current vcl-ut policy. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 5, 2026
…transitive cycle (#52) Reconciles the parked `claude/abi-tier2-and-l10-trans-cycle` branch into `main` (branch-reconciliation pass, owner-approved). Unmerged since 2026-06-03. Substantive proof/ABI work: - `src/interface/abi/Tier2.idr` (+209) — Tier-2 Idris bindings - `src/core/Decide.idr` (+79) — closes the **L10 transitive cycle** - retires legacy `abi/Foreign.idr` → `legacy/Foreign.idr` - `verification/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 current `main` (post #48/#49/#50, incl. the licence normalisation). https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- _Generated by [Claude Code](https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME)_ Co-authored-by: Claude Opus 4.7 (1M context) <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
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.
Normalises licence headers to current policy.