ci(governance): refresh stale standards reusable pins → fix Hypatia + staleness CI#107
Merged
Merged
Conversation
… prerequisite)
normalizedIsSafe was false AS STATED, not merely unproven: SafePath's grammar
(SafeEmpty | SafeComponent c rest => c ++ "/" ++ rest) only admits trailing-slash
paths {"", "a/", "a/b/"}, while normalizePath (split/filter/joinBy) produces NO
trailing slash {"", "a", "a/b"}. The two languages overlap only at "", so
SafePath (normalizePath p) was uninhabited for every non-empty path — the
idris_crash postulate masked an impossible theorem.
Redesign SafePath to model normalized relative paths correctly:
- SafeSingle: a single FINAL component (the no-trailing-slash leaf).
- SafeComponent now also requires a NON-EMPTY rest (so the only leaf is
SafeSingle, forcing every "/"-segment through the per-component checks).
- Each component must be '/'-free, expressed as Not (charsElem '/' (unpack c) =
True) over List Char (provable, reduces; no opaque isInfixOf, no Char-eq axiom).
This is load-bearing for SOUNDNESS: with only "doesn't start with /", a single
"component" like "a/../x" would sneak a ".." past the not-".." check.
absolutePathRejection re-proven against the 3 constructors via a new
slashPrefixImpliesCharsElem bridge (prefixNative + nonEmptyUnpack + andLeftTrue +
charsElemHere) — no new trusted base, Bool-level only. Build green (cerro-torre.ipkg
7/7). normalizedIsSafe stays a now-correctly-typed postulate; its discharge
(verified joinBy + splitNoDelim/dotDotInfixOfJoin axioms) is the next step.
https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
…ostulate Step 2 of §3 (after the SafePath redesign in d7f07fb). normalizedIsSafe is now a real proof, not an idris_crash: normalizedIsSafe p noDot = joinBySafe (normComponents p) (mkAllSafe p noDot) - joinBy lifted to top level (renamed joinSep to avoid the Data.String.joinBy clash) and shared with normalizePath via normComponents, so normalizePath p reduces definitionally to joinSep "/" (normComponents p). - joinBySafe builds SafePath of the join from per-component safety; SafeEmpty/ SafeSingle/SafeComponent line up with joinSep's []/[x]/(x::y::ys) clauses. - mkAllSafe derives, for each component: non-empty (filterSat), not ".." (else dotDotInfixOfJoin contradicts the premise), '/'-free (splitNoDelim + allFilter). - ~13 supporting lemmas (filterSat, allFilter, allElem, allFromElem, appendEmptyLeft, joinByConsNonEmpty, the Bool/String micro-lemmas) are all total — they add nothing to the trusted base. Trusted base grows by EXACTLY two fundamental opaque-String-primitive axioms: splitNoDelim — split (== '/') yields '/'-free components dotDotInfixOfJoin — a ".." component is a ".." infix of the join Both are genuine backend-semantics facts with no Idris2 reduction rules, in the same justified category as the existing isPrefixOfBridge/unpackAppend bridges. No believe_me / cast Refl / assert_total. cerro-torre.ipkg builds 7/7 green. PROOF-NEEDS.md updated (17 partial sites; normalizedIsSafe -> PROVEN). https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
…laims Reconcile the AffineScript/Ephapax threads as complementary roles, not competitors, and align stale status docs with verified ground truth. - Language policy (svalinn, cerro-torre, vordr component CLAUDE.md): AffineScript = primary general application language (ReScript replacement, typed-wasm); Ephapax = linear security core (exactly-once tokens, revocation, secret/handle lifecycle, container-lifecycle invariants, zero-copy IPC). Adds an Ephapax row to each ALLOWED-languages table. - stapeln.toml: svalinn component description + language note now reflect the in-flight ReScript -> AffineScript (general) + Ephapax (linear core) migration (11/33 modules ported). - ECOSYSTEM-STATUS.md: 2026-01-25 snapshot marked stale; selur ephapax/bridge.eph + types.eph are implemented (the "NOT EXISTS" line is obsolete). - READINESS.adoc: Idris2 proofs are real (33 .idr, no believe_me/postulate), not "stubs only".
…tructor-link fix
The svalinn AffineScript migration blocker is NOT affinescript #138 (closed,
PR #193 — the resolver/typecheck half). The real blocker is an untracked
WASM-codegen gap: gen_imports never linked imported enum constructors, so
`use prelude::{Some, None}` consumers failed `compile` with
Codegen.UnboundVariable despite passing `check`. Implemented + verified the fix
locally against affinescript HEAD 58dc2a0 (458-test suite green incl. a new
WASM-target regression test; zero regressions on the conformance+modules corpus).
Persists the git-apply-able patch, a before/after repro script, and the
ready-to-file new-issue text so it survives container reclaim and a future
affinescript-scoped session can land it. Refs #96.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
…mpiler + re-pin
SOURCE (container-stack/svalinn/src):
- Add explicit `use prelude::{Option, Some, None[, Result, Ok, Err]}` to the 6
modules using those value constructors. They were ported against the old
affinescript where Some/None/Ok/Err were seeded builtins; #138 (PR #193)
removed that seed, so constructors must now resolve through the module path.
AuthTypes + GatewayTypes now compile to WASM (4/11, was 2/11).
- Metrics: string concat `+` -> `++` (`+` is Int-only) and `let` -> `let mut`
for reassigned locals. Now passes parse+typecheck; remaining blocker is the
upstream WASM `float_to_string` builtin gap.
TOOLCHAIN (re-pin):
- Bump AFFINESCRIPT_REF d2875a5 (does not build — menhir r/r conflict) ->
58dc2a0 (current HEAD, verified building) in the workflow, Containerfile, and
migration task doc.
- Carry the vetted WASM cross-module constructor-linking patch (merged in #105)
in the build until it lands upstream in affinescript; then drop the apply and
bump the pin to the merged SHA.
Verified locally (affinescript 58dc2a0 + the patch): 4/11 modules compile to
WASM. Remaining blockers: 4 parse errors (Main/Json/PolicyEngine/Client —
unsupported syntax), 2 sibling-module resolutions (Authz/SecurityHeaders —
single-file compile has no src/** search path), 1 upstream WASM builtin gap
(Metrics float_to_string). Refs #96.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
…fe5a) The `governance / Check Workflow Staleness` gate flagged the governance, Hypatia, and Scorecard reusable workflows as pinned to a pre-cache/baseline-fix standards SHA — which is why `scan / Hypatia Neurosymbolic Analysis` died at "Prepare all required actions" (unresolvable actions/cache@d4373f26… inside the old reusable). hyperpolymath/standards already fixed it upstream; bump the three flagged pins to current standards HEAD d72fe5a. (scorecard-enforcer.yml was already removed on main.) Fixes the estate-wide Hypatia + workflow-staleness CI failures. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
|
hyperpolymath
pushed a commit
that referenced
this pull request
Jun 21, 2026
…urrent HEAD) The workflow-staleness gate tracks standards HEAD, which advanced since #107. Refresh governance/hypatia/scorecard reusable pins to keep the gate green. (This is a moving target — recommend automating via the estate's sha_bump_propagation rather than a manual per-PR bump.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
hyperpolymath
added a commit
that referenced
this pull request
Jun 21, 2026
## What Adds `SPDX-License-Identifier: MPL-2.0` (stapeln's canonical identifier — 1010 existing uses) to **303 stapeln-owned source/doc files** that lacked one. This clears the bulk of Hypatia's `missing_spdx` findings — the largest contributor to the 342 the scan surfaced once #107 re-enabled it. Per-type comment styles (verified against existing headers): `<!-- -->` (`.md`), `//` (`.adoc`/`.zig`), `#` (`.sh`/`.yml`/`.toml`/`.a2ml`/`.nix`/`.ex`/`.exs`), `;` (`.scm`). Inserted **after shebangs**, and **after YAML frontmatter** for 6 issue-template / `site` `.md` files so GitHub template parsing isn't broken. **Deliberately excluded:** generated output (`.cmj`/`.ttm`/`.po`, `lib/bs/`), comment-less formats (`.json`/`.jsonl`), license texts (`LICENSES/`, `LICENSE-*`), `.well-known/*` standard files, `frontend`/`dom-mounter` `.js` (ReScript-migration zone — may be generated), and the legacy `.res` corpus. ## On the `http://` half — no conversions (intentional) I investigated all **46** `http://` occurrences; **none should be converted**. They're all intentional: - **security-test attack URLs** — `evil.com`, `attacker.com`, `169.254.169.254` (cloud-metadata SSRF) in `RED-TEAM-EXERCISE.md` / `OBVIOUS-VULNERABILITIES.md` - **internal service refs** — `http://backend`, `http://vordr`, `http://svalinn`, `*.internal`, `*.local` - the **MPL-2.0 license text** (`mozilla.org`), the **Apple plist DTD identifier**, `example.org`/`yoursite.com` placeholders - the **aspect-test that literally greps for `http://`** Converting any would corrupt security fixtures, break internal refs, or edit the license. The right resolution for these is a `hypatia:ignore http_in_docs` pragma or baseline entry — **not** a find-replace. I can add those pragmas if you want; I didn't do it unprompted since each needs a per-case reason. ## Verification 303 files changed, 303 insertions (exactly one header each); 0 shebang-placement errors; 0 double headers; frontmatter files re-checked. Refs #96. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z --- _Generated by [Claude Code](https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z)_ --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: hyperpolymath <paraordinate@yahoo.co.uk>
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.
What
Bumps the three flagged
hyperpolymath/standardsreusable-workflow pins from the pre-cache-fix SHA5a93d9d→ current standards HEADd72fe5a:governance.yml→governance-reusable.ymlhypatia-scan.yml→hypatia-scan-reusable.ymlscorecard.yml→scorecard-reusable.ymlWhy
The
governance / Check Workflow Stalenessgate explicitly demanded this ("Refresh to current standards SHA"), and it's the root cause of the estate-wide red that's been failing every stapeln PR:That broken
actions/cachepin lives inside the old standards reusable workflow —hyperpolymath/standardsalready fixed it atd72fe5a, but stapeln pinned the pre-fix SHA. So this single change clears bothscan / Hypatia Neurosymbolic Analysisandgovernance / Check Workflow Staleness.Notes:
scorecard-enforcer.ymlwas already removed onmain.secret-scanner/spark-theatre-gate/mirrorpins were not flagged by the staleness gate, so they're left untouched.This is the "bump broken actions to sort" follow-up to the merged #106 (svalinn ports + compiler re-pin).
🤖 Generated with Claude Code
https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
Generated by Claude Code