fix(svalinn): port gateway modules off pre-#138 compiler + re-pin (4/11 compiling)#106
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
|
hyperpolymath
added a commit
that referenced
this pull request
Jun 21, 2026
… staleness CI (#107) ## What Bumps the three flagged `hyperpolymath/standards` reusable-workflow pins from the pre-cache-fix SHA `5a93d9d` → current standards HEAD `d72fe5a`: - `governance.yml` → `governance-reusable.yml` - `hypatia-scan.yml` → `hypatia-scan-reusable.yml` - `scorecard.yml` → `scorecard-reusable.yml` ## Why The `governance / Check Workflow Staleness` gate 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: ``` scan / Hypatia Neurosymbolic Analysis → ##[error]Unable to resolve action `actions/cache@d4373f26…`, unable to find version ``` That broken `actions/cache` pin lives **inside the old standards reusable workflow** — `hyperpolymath/standards` already fixed it at `d72fe5a`, but stapeln pinned the pre-fix SHA. So this single change clears **both** `scan / Hypatia Neurosymbolic Analysis` and `governance / Check Workflow Staleness`. Notes: - `scorecard-enforcer.yml` was already removed on `main`. - The `secret-scanner` / `spark-theatre-gate` / `mirror` pins 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.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>
hyperpolymath
added a commit
that referenced
this pull request
Jun 21, 2026
…ATE.a2ml + runbook) (#109) ## What Closes the documentation gap flagged while wrapping up: the AffineScript-migration outcome lived only in merged-PR bodies (#105/#106) and chat, while the repo's durable **apparatus** understated reality. - **`STATE.a2ml`** previously said `# No blockers recorded` → now records the real blocked-on-upstream WASM constructor-link dependency (carried patch over `58dc2a0`; #105), the **4/11** gateway-compile status, the specific parse / sibling-resolution / `float_to_string` blockers, and ordered `[critical-next-actions]`. - **`AFFINE-MIGRATION-TASK.md`** gains a dated **Current status** section with the same, superseding the stale PR #46 framing. A future session reading `STATE.a2ml` + the runbook is now self-sufficient — no need to dig through merged PRs. Docs-only. 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.
Summary
Builds on #105 (the merged WASM cross-module constructor-link fix). Two halves.
Source ports (
container-stack/svalinn/src)use prelude::{Option, Some, None[, Result, Ok, Err]}to the 6 modules using those value constructors — they were ported against the pre-#138 seeded-builtin compiler; affinescript #138 (PR #193) removed the seed, so constructors must now resolve through the module path.AuthTypes+GatewayTypesnow compile to WASM → 4/11 (was 2/11).Metrics: string concat+→++(+is Int-only here) andlet→let mutfor reassigned locals. Now passes parse+typecheck; blocked only on the upstream WASMfloat_to_stringbuiltin.Re-pin (
svalinn-affine-build.yml,Containerfile,AFFINE-MIGRATION-TASK.md)AFFINESCRIPT_REFd2875a5(does not build — menhir reduce/reduce conflict) →58dc2a0(current HEAD, verified building).git applys the vetted constructor-link patch (merged in maintenance: proven affinescript WASM constructor-link fix (svalinn migration unblock) #105, staged atcontainer-stack/svalinn/patches/) 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:
AuthTypes,GatewayTypes,RateLimiter,VordrTypes.Remaining blockers (precisely characterized — none is the codegen fix)
Main(None => {}),Json(pub extern fn),PolicyEngine,Clientcompilehas nosrc/**search path)Authz,SecurityHeadersMetricsfloat_to_stringin the core-WASM codegen (upstream)The
svalinn-affine-buildgate stays red until those land (it requires all 11). This is honest, evidenced progress on the gateway port + a functional toolchain pin. Draft for review.🤖 Generated with Claude Code
https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
Generated by Claude Code