vcl-ut Phase 4: discharge layout + L6-L10 join-closure proof debt (standards#124)#24
Merged
Merged
Conversation
New self-contained module VclTotal.ABI.LayoutProofs (10th ipkg module, CI-gated). Discharges the three Phase-3c-deleted unsound items honestly: - alignToDivides: a divides alignTo size a, GENUINE by construction (alignTo = ceil(size/a)*a = q*a, witness q; no div/mod lemma, no escape). Layout.alignUp additive↔ceil equivalence precisely scoped as alignUpAdditiveEquivOWED (documented, not faked) — user-approved opt A. - queryPlanHeaderNoPadding: sum of field sizes = 24 (genuine Refl over a concrete Vect, byte-identical to Layout.queryPlanHeaderLayout). - queryPlanHeaderWithin + fieldWithin: membership-quantified bounds via So / Data.So.soAnd (replaces the deleted ?offsetInBoundsProof hole). Root-caused two idris2 0.8.0 footguns that cost the prior loop: (1) 'total' is a reserved keyword — using it as a variable is the parse error reported downstream; (2) bare lowercase global in a type sig is auto-bound as a fresh implicit (qualify to pin). Module is self- contained (no Layout import) to avoid record-projection shadowing. Clean build EXIT=0 (10/10), zero proof-escapes, SafetyL4Model checks. Refs hyperpolymath/standards#124. Does not close. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… discharged Completes the Phase-4 proof-debt work (hyperpolymath/standards#124). The VclTotal proof corpus now machine-checks GREEN as 10 modules under idris2 0.8.0 (`idris2 --build verification/proofs/vclut-core.ipkg`, exit 0, %default total), with ZERO proof-escape symbols (CI-enforced: no believe_me / really_believe_me / postulate / assert_total / assert_smaller / idris_crash / sorry). src/core/Composition.idr - L6-L9 join-closure: l6/l7/l8/l9Compose given explicit unrestricted {q1,q2 : Statement} binders (were erased auto-implicits, used at runtime); presentJoinEffects/Version helpers reordered before use. - ifNilForcesTrue: explicit {0 a : Type} + pinned list type. - fuaSuperset / fuaNilAppend EpReqEntails clauses rewritten as genuine nested `with (agentDeclared aN d) proof` case splits (the prior let-bound-`if` rewrite did not reduce); False branches discharge via `absurd` on the [agentId a] contribution. - epiStructJoin: ambiguous type-ascribed `let` removed; new genuine helpers undeclaredCaseNil / nilUndeclaredCase (case-fold <-> `= []` round-trip) + epiStructDecl1/2 (superset monotonicity lift). - L10 no-ENTAILS-cycle non-closure unchanged: still the explicit minimal JoinSideCondition (stated in the type, never faked). src/core/Decide.idr - findUndeclaredAgents EpReqEntails clause inlined (no `let u1/u2`); definitionally identical, exposes the `if` subterms so the Composition-side case splits reduce. src/core/{Checker,Levels}.idr - Phase-4b WIP carried in this branch (L6-L10 predicates over the shared Decide deciders); compiles clean. verification/proofs/VERIFICATION-STANCE.adoc - Truth maintenance: Phase 4a (LayoutProofs: alignToDivides, queryPlanHeaderNoPadding, fieldWithin) and Phase 4b (L6-L10 composeJoin closure) marked RESOLVED in the OWED/roadmap/ provenance sections; the additive<->ceil alignUp sliver and the L9/L10 predicate-depth items remain precisely scoped (not faked). Verified independently: clean-`build/` rebuild, all 10 modules, exit 0; CI-identical proof-escape audit clean. Refs hyperpolymath/standards#124 (does NOT close the epic). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Brings the human-facing docs in line with the now-verified state (Phases 1–3 on main via #21/#22/#23; Phase 4 = PR #24). No source or proof changes; corpus remains green (10 modules, exit 0, zero escapes). - PROOF-NEEDS.md: the false "corpus does not compile / never machine-checked / L2/L3/L5 vacuous" block replaced with the actual CI-gated 10-module state; per-level status corrected (L1–L10 resolved, residual gaps precisely scoped). - verification/proofs/README.adoc: added `vclut-core.ipkg` to Contents + the corpus build to "Verifying"; corrected the STANCE summary. - verification/proofs/VERIFICATION-STANCE.adoc: headline updated "Phase 1 + 2 + 3" -> "Phase 1–4". - CHANGELOG.md: new "### Verified" entry under [Unreleased] recording the Phase 0→4 proof-corpus remediation. The a2ml machine manifests carry no verification state (generic scaffolding) and were correctly left untouched. VERIFICATION-STANCE.adoc remains the authoritative catalogue and takes precedence over README/PROOF-NEEDS prose. Refs hyperpolymath/standards#124. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…then obsolete; user-approved) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
9 tasks
Boundary-reinforcement workstream (FFI proof-attestation transport + missing String->Statement parser; secondary OWED items) is now tracked in #25 rather than only narrated. No source/proof change; corpus stays green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,168 @@ | |||
| -- SPDX-License-Identifier: PMPL-1.0-or-later | |||
🔍 Hypatia Security ScanFindings: 22 issues detected
View findings[
{
"reason": "Issue in quality.yml",
"type": "missing_workflow",
"file": "quality.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in security-policy.yml",
"type": "missing_workflow",
"file": "security-policy.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Action idris-community/setup-idris@v1 needs attention",
"type": "unpinned_action",
"file": "proof-corpus.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action actions/upload-artifact@v4 needs attention",
"type": "unpinned_action",
"file": "release.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action actions/download-artifact@v4 needs attention",
"type": "unpinned_action",
"file": "release.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "codeql.yml lists `language: javascript-typescript` but the repo has no source files in any CodeQL-scannable language. The analyze job will exit 'no source files' on every run. Switch the matrix to `actions` (which scans workflow files — every repo has those).",
"type": "codeql_language_matrix_mismatch",
"file": "codeql.yml",
"action": "switch_codeql_matrix_to_actions",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "assert_smaller bypasses termination checker (1 occurrences, CWE-704)",
"type": "assert_smaller",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Checker.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "believe_me undermines formal verification (2 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Decide.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "believe_me undermines formal verification (3 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Composition.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
… action) The idris-community/setup-idris action repo no longer resolves (404), failing the proof-corpus gate at action-resolution in ~2s (NOT a proof regression; corpus verified green locally). Replace with a SHA-pinned source build of idris-lang/Idris2 v0.8.0 (15a3e4e70843f7a34100f6470c04b791330788df) + chezscheme: deterministic, version-exact, no third-party action. Refs hyperpolymath/standards#124. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 21 issues detected
View findings[
{
"reason": "Issue in quality.yml",
"type": "missing_workflow",
"file": "quality.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in security-policy.yml",
"type": "missing_workflow",
"file": "security-policy.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Action actions/upload-artifact@v4 needs attention",
"type": "unpinned_action",
"file": "release.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action actions/download-artifact@v4 needs attention",
"type": "unpinned_action",
"file": "release.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "codeql.yml lists `language: javascript-typescript` but the repo has no source files in any CodeQL-scannable language. The analyze job will exit 'no source files' on every run. Switch the matrix to `actions` (which scans workflow files — every repo has those).",
"type": "codeql_language_matrix_mismatch",
"file": "codeql.yml",
"action": "switch_codeql_matrix_to_actions",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "assert_smaller bypasses termination checker (1 occurrences, CWE-704)",
"type": "assert_smaller",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Checker.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "believe_me undermines formal verification (2 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Decide.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "believe_me undermines formal verification (3 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Composition.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
"type": "assert_total",
"file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Composition.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
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.
Phase 4 — discharge the Phase-3 "owed" layout + L6–L10 join-closure debt
Closes out the Phase-4 proof-debt of the
vcl-utverification remediation(hyperpolymath/standards#124). Does not close the epic — that is the
user's call.
Result (verified independently, twice, from a clean
build/)idris2 0.8.0 --build verification/proofs/vclut-core.ipkg→ exit 0,all 10 modules typecheck under
%default total, zero proof-escapesymbols (CI-identical audit: no
believe_me/really_believe_me/postulate/assert_total/assert_smaller/idris_crash/sorry). The previously-failing module wasVclTotal.Core.Composition(uncommitted Phase-4b WIP); it now builds, as do
Checker,LayoutProofs, andLayoutafter it.Phase 4a —
VclTotal.ABI.LayoutProofs(committed2aa931e)Genuine, self-contained, CI-gated (10th ipkg module) replacements for
the three unsound Phase-3c-deleted items:
alignToDivides— alignment divisibility by construction for thecanonical round-up-to-multiple form
alignTo size a = ⌈size/a⌉ * a(witness = the quotient; no
div/modlemma, no escape).queryPlanHeaderNoPadding— Σ field sizes (4+4+4+4+8) = declaredcap 24, reduces under
Refl(byte-identicalPFieldmodel).queryPlanHeaderWithin/fieldWithin— membership-quantified boundvia
Data.Vect.Elem+Data.So.soAnd(honest replacement for thedeleted false
offsetInBounds/?metavariable).Layout.alignUp↔ceil
alignToequivalence fora>0→ documentedStringnotealignUpAdditiveEquivOWED.Phase 4b — L6–L10
composeJoinclosure (commit4d236e9)L6–L10 predicates carry the shared
VclTotal.Core.Decidedeciders andare genuinely closed under
composeJoin, machine-checked:l6/l7/l8/l9Compose— present-LIMIT/EFFECTS/VERSION join + all fourENFORCED×ENFORCED
joinLinearcases (fixed: erased auto-implicits{q1,q2}made unrestricted;presentJoin*helper ordering).epiStructJoin— L10 structural part (clause present, ≥1 agent,every requirement agent declared) via genuine superset monotonicity
(
fuaSuperset/agentDeclaredAppL/agentDeclaredAppR,fuaNilAppend,the
undeclaredCaseNil/nilUndeclaredCasecase-fold round-trip).ENTAILS-cycle sub-property is provably notjoin-closed and stays carried by the explicit minimal
JoinSideCondition— stated in the type, never faked (unchanged).Decide.findUndeclaredAgentsEpReqEntailsinlining (droplet u1/u2) so the case splits reduce.verification/proofs/VERIFICATION-STANCE.adocupdated for truthmaintenance: Phase 4a/4b marked RESOLVED in the OWED / roadmap /
provenance sections; the additive↔ceil sliver and the L9/L10
predicate-depth deepening remain precisely scoped as future work.
Merge oracle
The
idris2 --buildofvclut-core.ipkg(here: the CI Proof Corpusworkflow). Do not admin-merge past a non-green build.
Refs hyperpolymath/standards#124.
🤖 Generated with Claude Code