Repository navigation
fix(ci): unblock E2E Validation and Static Analysis Gate (actions.lock drift from #268) - #270
Merged
Merged
Conversation
… again E2E Validation and Static Analysis Gate have been `startup_failure` on main since 554345c (#268): Dependabot bumped setup-node 7.0.0 -> 7.1.0, upload-artifact 7.0.1 -> 7.0.2, download-artifact 8.0.1 -> 8.0.2 and setup-ocaml 3.8.0 -> 3.9.0 without a lock refresh, the same failure #266 fixed two commits earlier. A ref absent from .github/workflows/actions.lock is a ref the organisation does not allow, so the workflow is rejected before any job runs. This reverses exactly #268's four workflow edits, back to the refs the lock declares. It does not prevent recurrence: the next grouped actions bump will drift again unless the lock is regenerated with it (owner decision). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
With E2E Validation able to start again, its structural and smoke jobs
fail on paths that moved without the tests following (pre-existing on
main, masked by the startup_failure):
tests/e2e.sh LEVEL-STATUS.md -> LEVEL-STATUS.adoc, and the
row pattern "| N |" (Markdown) -> "^|N |"
(AsciiDoc), so all 12 rows are really checked
tests/aspect/claim-envelope LEVEL-STATUS / PROOF-NEEDS / TEST-NEEDS .md
-> .adoc in the RSR list and the L11/L12
cross-check
tests/aspect/security-envelope .well-known/security.txt
-> www/.well-known/security.txt
README.adoc, ROADMAP.adoc docs/WHITEPAPER.md -> docs/WHITEPAPER.adoc
Locally: tests/e2e.sh (E2E_BUILD=0) 47 passed / 0 failed (was 35 / 1),
claim-envelope 57 / 0 (was 51 / 5), security-envelope 10 / 0 (was 9 / 1).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Contributor
|
Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configuration
📒 Files selected for processing: 9
✨ Finishing Touches
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Merged
11 of 12 tasks
|
hyperpolymath
marked this pull request as ready for review
October 14, 2026 01:04
hyperpolymath
added this pull request to stack #272
October 14, 2026 01:05
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
…ax-plus (PWL-01, PR A) (#271) ## Summary PWL-01 step 1. This ports hyperpolymath/resource-algebra `Core.agda` and its three instances to Idris2 as the ABI's grade kernel. `Tropical.idr` and `Echo.idr` now draw their grades from it, and a grep gate enforces one definition of min-plus and one of max-plus in the tree. Stacked on #270, the CI unblock. Without it, E2E Validation can't start. Pin: resource-algebra `cf9235c532712a783a404c359a1055f40134794a`, fetched by `scripts/fetch-siblings.sh`. **One correction to the issue text.** `Tropical.idr` was never max-plus. Its `TropCost` is min-plus, the same algebra as **Loss**. Its bottleneck layer (`tropMax`) is min-max, which is neither min-plus nor max-plus. So both `Tropical.TropCost` and `Echo.EchoGrade` became the **Loss** carrier. **MaxPlus** is in the kernel, but no L11 obligation uses it yet. `tests/reject/TropicalIsNotMaxPlus.idr` is the checked statement. ## Changes - `src/abi/TypedWasm/ABI/ResourceAlgebra.idr`: the `ResourceAlgebra` interface. `IsOrdered`, `IsDioid` and `IsAnnihilating` are separate interfaces, as in Agda. "Every dioid is ordered" is a proof: `dioidMonoL`/`R` and the named implementation `dioidOrdered`. A transcription map is in the header. - `ResourceAlgebra/{Loss,MaxPlus,HWM}.idr`: clause-for-clause transcriptions. Constructors are renamed `fin/inf` → `Finite/Infinity` and `val/bot` → `Val/Bot`; clause order is kept. `Separation.idr` has S-1..S-3. `Nat.idr` holds only the lemmas base lacks: base's `Data.Nat.minimum`/`maximum`/`LTE` *are* the Agda Prelude's `min`/`max`/`≤`, so the tree declares no Nat min/max at all. - `Tropical.idr`: `TropCost = LossGrade`. The 12 axioms and the order layer are derived from the kernel, and `tropMin`/`natMax` are deleted. Every public name is kept, so `Epistemic`/`Proofs` compile unchanged. `Echo.idr`: `EchoGrade = LossGrade`. - `tools/check-grade-kernel.sh` is the grep gate. Its `--self-test` is the negative control: 8 seeded duplicates are caught, 0 false positives. Run on `main`'s `Tropical.idr`, it fails. `tools/grade-kernel.allow` holds the one exception (`tropMax`, MinMax) with its reason. - `tools/check-kernel-proofs.sh` runs the falsifiers. A missing toolchain fails the gate; it never skips: - upstream `check-agda.sh` at the pin; - a clean `idris2 --build`; - `tests/reject/*.idr`, each refused at its `invalid` line with its `EXPECT` message; - the transcription table `tests/transcription/ops.tsv`: 172 rows, Agda `refl` against the pinned sources and Idris2 `Refl` against the port, with `wrong-rows.tsv` refused by both. - CI: two new jobs in `contract-gate.yml`. They go there, not in a new workflow, because `actions.lock` is keyed by path. Idris2 0.8.0 is built from its tag because there are no binaries. - Docs: `LEVEL-STATUS` row 11, the inventory and a new "Grade kernel" section; `CONTRACT` Enforcement; the spec's L11 sentence; `CHANGELOG`. `regression.mjs` pins 31 kernel names. ## Status rows (artefact for each) | Claim | Status | Artefact | |---|---|---| | Kernel laws (C-1–C-4, L-1, M-1, H-1 restated in Idris2) | PROVEN (Idris2) | `ResourceAlgebra*.idr`, `idris2 --build` | | Port ≡ Agda source | ASSUMED, TESTED on 172 rows / 244 equalities | `tools/check-kernel-proofs.sh` step 4 | | S-1–S-3 separation | TESTED (computed) | `ResourceAlgebra/Separation.idr` | | C-4 / H-3 (HWM has no annihilating zero) | TESTED | `tests/reject/HWMAnnihilates.idr` | | L11 / L12 | **unchanged: draft** | none | ## RSR Quality Checklist ### Required - [x] Tests pass (see Testing) - [x] Code is formatted - [x] Linter is clean: the build has the same 24 warnings as `main`, none new - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments - [x] No banned functions: zero `believe_me`/`assert_total` (checked by the gate) - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable - [ ] `.machine_readable/descriptiles/STATE.a2ml` not updated: last updated 2026-05-27, and its completion figures are hand-written; left for the owner - [x] Documentation updated - [x] `CHANGELOG` updated - [x] ABI changes validated. `contract.abi.sha256` is **unchanged**: the I3 anchors cover `section.rs`'s wire format, not `src/abi/` (now stated in `CONTRACT.adoc`). Re-sealing without an `abi_version` bump would be wrong. ## Testing ``` tools/check-contract.sh OK: contract gate — I1 + I3 hold tools/check-grade-kernel.sh --self-test PASS 8/8 seeded duplicates; kernel shapes accepted; 0 false positives tools/check-grade-kernel.sh OK: one definition of min-plus (ResourceAlgebra/Loss.idr) and one of max-plus (ResourceAlgebra/MaxPlus.idr); no Nat min/max outside base tools/check-kernel-proofs.sh OK: kernel proofs — build, 4 rejection(s), table, and 3 negative control row(s) node tests/proof/regression.mjs --strict 172 passed, 0 failed, 0 skipped ``` Mutation check: hand-corrupting one row of `ops.tsv` fails the gate three ways (explorer drift, Agda refusal, Idris2 refusal) and exits 1. **Decisions for the owner:** 1. MinMax (bottleneck) has no kernel instance. Should one be added upstream? 2. This PR adopts the open question's checker-matches-explorer option. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- _Generated by [Claude Code](https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
pushed a commit
that referenced
this pull request
Oct 14, 2026
…uash merges) #270 and #271 were squash-merged into main, so their commits on this branch are not ancestors of main. Merging main back in (rather than force-pushing a rebased branch) keeps the branch's published history; the trees agree except for the SPDX header commit, which is not yet on main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
hyperpolymath
pushed a commit
that referenced
this pull request
Oct 14, 2026
cargo-verify (E2E Validation) fails before compiling anything:
error: failed to parse lock file ... package `wasmparser` is
specified twice in the lockfile
Three Dependabot PRs (#231 wasm-encoder, #232 wasmprinter, #233
wasmparser), each moving to 0.256.0, merged on top of each other and left
two `wasmparser 0.256.0` entries plus a stale 0.255.0 one that a crate
still pointed at. It went unseen because E2E Validation was
startup_failure until #270.
The lock was rewritten by cargo itself (`cargo metadata` after dropping
the duplicated entry), not by hand: one dependency edge 0.255.0 -> 0.256.0,
the 0.255.0 entry and the duplicate removed, nothing upgraded.
`cargo build --workspace --locked` and `cargo test --workspace --locked`
pass (all test binaries ok).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
11 of 12 tasks
hyperpolymath
pushed a commit
that referenced
this pull request
Oct 14, 2026
governance / Actions lockfile verify fails on main and on every PR:
workflow uses ref "v0.5.0" but lockfile pins "v0.3.0"
(.github/workflows/push-email-notify.yml)
Dependabot #265 bumped hyperpolymath/smtp-notify-action v0.3.0 -> v0.5.0
without a lock refresh, the same drift #266 and #270 reverted elsewhere
(#270 left this one alone because #268 did not cause it). Back to the
locked v0.3.0; recurrence needs the lock refreshed with the bump (owner
decision, as in #270).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
…-2 at a boundary (PWL-01, PR B) (#273) ## Summary PWL-01 steps 2–3, on top of the kernel from #271 (merged). L11 and L12 obligations are restated against the grade kernel, and L13 gets the occupancy reading: occupancy-types' reclamation law (R-2), ported and re-proved, then bound to `private_memory` and `boundary`. **No row moves to achieved**; L11/L12 stay draft. One correction carried from PR A: the issue asks for "`Level11BottleneckProof` as MaxPlus", but the bottleneck is MinMax, not MaxPlus. Restating it as MaxPlus would change its meaning at an unreachable (+∞) edge. So the bottleneck stays as it is, and MaxPlus goes where max-plus is the right algebra: a worst case over branches. Pins: resource-algebra `cf9235c`, occupancy-types `af957280075699c659de0abd9a3b0defade77309` (both in `scripts/fetch-siblings.sh`). ## Changes - **L11** (`Tropical.idr`): - `CostBounded c n` is proved to *be* the Loss order `Finite n ≼ c` (`costBoundedIsLossOrder` / `lossOrderIsCostBounded`). - Path bounds compose by the kernel's `otimesMono` (`costBoundedSeq`). - New `Level11WorstCaseProof` grades a branching `AccessPlan` in MaxPlus, with `worstCaseThen` / `worstCaseOneOf` from `otimesMono` / `oplusMono` and `worstCaseFinite` / `worstCaseWithin`. The obligation is **DESIGNED**: no surface syntax or attestation uses it. - **L12** (`Epistemic.idr`, additive): `stalenessGrade` is the reader's lag as a Loss grade. - Fresh = 𝟙 (`freshHasNoStaleness`), stale ≠ 𝟙 (`staleHasStaleness`), never synced = 𝟘 (`neverSyncedIsCollapse`). - 𝟙 is the top (`freshIsTop`), and relayed lag = ⊗ (`stalenessRelay`). - `syncGrade` gets a note: it holds a version, not a loss. - **L13** (new `Occupancy.idr`): occupancy-types R-1..R-5 ported and re-proved over the kernel's HWM (`cutFactor`, `reclaimLaw`, `occupancyAtCut`, `occupancyLeCost`, `noReclaim`, `reclaimed`, `witness*`). - Binding, **DESIGNED**: `OccupancyGradedMemory` (an HWM grade per private memory, within its declared maximum) and `BoundaryCut` / `boundaryFrees` = peak − drift / `boundaryOccupancy` / `fitsAcrossBoundary` (the budget rule across a boundary). - `striated` occupancy stays OPEN: it's a surface-only construct. - **Kernel additions**, typed-wasm's own and labelled (no operation changes, so the transcription table is unchanged): each instance's order read in ℕ (`lossLeOfLTE`, `maxPlusLeOfLTE` + inverses); `maxLub` and min/max-vs-`LTE` lemmas in `ResourceAlgebra/Nat.idr`. - **Rejects**: `CostIsOccupancy`, `DriftIsPeak` (occupancy-types R-6), `WorstCaseIsCheapest`. `tools/check-kernel-proofs.sh` also runs occupancy-types' own Agda check at its pin, against our resource-algebra pin. - `LEVEL-STATUS` rows 11–13 name the kernel artefacts; new inventory row; `CHANGELOG`; 18 names pinned in `regression.mjs`. - **CI repair, own commit** (`e080ef6`): `Cargo.lock` listed `wasmparser` twice. Three concurrent Dependabot bumps (#231–#233) caused it, and it was invisible while E2E was `startup_failure`. Once #270 landed, **E2E Validation / cargo-verify went red on `main`** with `package wasmparser is specified twice in the lockfile`. The lock was rewritten by cargo itself: one edge 0.255.0 → 0.256.0, the stale and duplicate entries removed, nothing upgraded. `cargo build --workspace --locked` and `cargo test --workspace --locked` pass. Branch note: this is the designated branch after #271's squash merge. `main` was merged back in (`bb2380b`) instead of force-pushing; the tree equals a clean rebase on `main`. ## Status rows (artefact for each) | Row | Claim | Status | Artefact | |---|---|---|---| | 11 | bound = Loss order; bounds compose | PROVEN | `costBoundedIsLossOrder`, `costBoundedSeq` | | 11 | worst-case obligation (MaxPlus) | PROVEN lemmas, obligation DESIGNED | `Level11WorstCaseProof`, `worstCaseThen/OneOf`; `tests/reject/WorstCaseIsCheapest.idr` | | 12 | staleness as Loss | PROVEN | `freshHasNoStaleness`, `staleHasStaleness`, `stalenessRelay` | | 13 | R-1..R-5 (occupancy-types `Reclaim`/`Timeline`/`Witness`) | PROVEN in Idris2; correspondence ASSUMED (port-and-reprove) | `Occupancy.idr`; upstream check at `af95728` in the gate | | 13 | R-6 | TESTED | `tests/reject/{CostIsOccupancy,DriftIsPeak}.idr` | | 13 | binding to `private_memory` / `boundary` | DESIGNED | `OccupancyGradedMemory`, `BoundaryCut` | | 13 | `striated` occupancy | OPEN | none | ## RSR Quality Checklist ### Required - [x] Tests pass (see Testing) - [x] Code is formatted - [x] Linter is clean (no new warnings) - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments - [x] No banned functions (gate checks zero `believe_me` / `assert_total` in the kernel) - [x] SPDX license headers present on all new/modified source files (incl. `CHANGELOG.adoc`, which had none) - [x] No secrets, credentials, or `.env` files included ### As Applicable - [ ] `.machine_readable/descriptiles/STATE.a2ml` not updated (stale since 2026-05-27; hand-written figures; owner's call) - [x] Documentation updated - [x] `CHANGELOG` updated - [x] ABI changes validated: `contract.abi.sha256` unchanged (I3 anchors are the wire format only) ## Testing ``` tools/check-contract.sh OK: contract gate — I1 + I3 hold tools/check-grade-kernel.sh OK: one definition of min-plus (ResourceAlgebra/Loss.idr) and one of max-plus (ResourceAlgebra/MaxPlus.idr); no Nat min/max outside base tools/check-kernel-proofs.sh OK: kernel proofs — build, 7 rejection(s), table, and 3 negative control row(s) PASS: upstream: PASS: core proofs and all 3 expected rejections PASS: upstream occupancy-types: PASS: core proofs and all 2 expected rejections PASS: idris2 --build typed-wasm.ipkg: 31 module(s) built, 0 errors node tests/proof/regression.mjs --strict 190 passed, 0 failed, 0 skipped E2E_BUILD=0 bash tests/e2e.sh 47 passed, 0 failed, 7 skipped cargo build/test --workspace --locked ok (all test binaries) ``` 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- _Generated by [Claude Code](https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t)_ --------- 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.
Summary
E2E Validation and Static Analysis Gate have been
startup_failureonmainsince554345c(#268). Dependabot bumped four workflow refs without refreshing.github/workflows/actions.lock. That is the same failure #266 fixed two commits earlier. A ref the lock doesn't list is one the organisation doesn't allow, so the workflow is rejected before any job runs.Getting the workflows to start exposes failures that have been sitting on
mainthe whole time. The tests point at files that have since moved. This PR fixes both. It's the bottom of the PWL-01 stack (the grade-kernel PR stacks on it), but it stands alone.Changes
13d26a5: reverts exactly chore(deps): bump the actions group with 4 updates #268's four workflow edits, back to the locked refs:setup-nodev7.1.0 → v7.0.0,upload-artifactv7.0.2 → v7.0.1,download-artifactv8.0.2 → v8.0.1,setup-ocamlv3.9.0 → v3.8.0.145d84b: points the tests at files that moved:tests/e2e.sh:LEVEL-STATUS.md→.adoc. The row pattern changes from| N |(Markdown) to^|N |(AsciiDoc), so all 12 rows are actually checked.tests/aspect/claim-envelope.mjs: the RSR list and the L11/L12 cross-check now useLEVEL-STATUS/PROOF-NEEDS/TEST-NEEDS.adoc.tests/aspect/security-envelope.mjs:.well-known/security.txt→www/.well-known/security.txt.README.adoc,ROADMAP.adoc:docs/WHITEPAPER.md→.adoc.RSR Quality Checklist
Required
unsafeblocks without// SAFETY:comments.envfiles includedAs Applicable
.machine_readable/descriptiles/STATE.a2mlupdated: no project-state changeCHANGELOGor release notes updated: CI-only fixTesting
Run locally on this branch, with the same commands the jobs run:
Not fixed here (owner decision): recurrence. The next grouped Dependabot actions bump will drift again unless the lock is regenerated alongside it. That needs
gh actions-lockplus the org allow-list publish, or a Dependabot rule holding theactionsgroup until the lock is refreshed. Other drifts are left alone because #268 didn't cause them. One example:push-email-notify.ymlusessmtp-notify-actionv0.5.0 while the lock says v0.3.0.🤖 Generated with Claude Code
https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Generated by Claude Code