maintenance: proven affinescript WASM constructor-link fix (svalinn migration unblock)#105
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
|
This was referenced Jun 21, 2026
hyperpolymath
added a commit
that referenced
this pull request
Jun 21, 2026
…11 compiling) (#106) ## Summary Builds on #105 (the merged WASM cross-module constructor-link fix). Two halves. ### Source ports (`container-stack/svalinn/src`) - Added `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` + `GatewayTypes` now compile to WASM → 4/11 (was 2/11).** - `Metrics`: string concat `+`→`++` (`+` is Int-only here) and `let`→`let mut` for reassigned locals. Now passes parse+typecheck; blocked only on the upstream WASM `float_to_string` builtin. ### Re-pin (`svalinn-affine-build.yml`, `Containerfile`, `AFFINE-MIGRATION-TASK.md`) - `AFFINESCRIPT_REF` `d2875a5` (does **not** build — menhir reduce/reduce conflict) → `58dc2a0` (current HEAD, verified building). - The build now `git apply`s the vetted constructor-link patch (merged in #105, staged at `container-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) | Class | Modules | Needs | |---|---|---| | Parse errors (unsupported syntax) | `Main` (`None => {}`), `Json` (`pub extern fn`), `PolicyEngine`, `Client` | source rewrites / upstream parser support | | Sibling-module resolution (single-file `compile` has no `src/**` search path) | `Authz`, `SecurityHeaders` | project/manifest build mode or a search-path flag (upstream) | | Upstream WASM builtin gap | `Metrics` | `float_to_string` in the core-WASM codegen (upstream) | The `svalinn-affine-build` gate 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.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.
What
Persists a verified,
git apply-able patch for the real blocker behind the svalinn AffineScript migration (#96), plus a before/after repro script and ready-to-file new-issue text, undermaintenance/affinescript-wasm-ctor-link/.Correction: the blocker is NOT affinescript #138
Checking #138 directly: it is closed (PR #193) and was the resolver/typecheck half ("remove the
b895374Some/None/Ok/Err seed; resolve imports recursively"). The actual blocker is an untracked WASM-codegen gap:gen_importslinked only importedTopFn/TopConst, neverTopType, so a module that doesuse prelude::{Option, Some, None}passescheckbut failscompilewithCodegen.UnboundVariable "… Some". Non-WASM backends useflatten_imports+ structural emission and were unaffected, and the stdlib AOT gate only compiles Deno-ESM — which is why the WASM gap went unguarded while epic #128/#131–#138 was marked done.The fix
lib/codegen.mlgen_importsnow registers imported public enum constructors intovariant_tagswith canonical positional tags (mirroring localTopTypehandling ingen_decl); globuse M::*brings enum constructors too; plus a WASM-target regression test (the coverage the Deno-only AOT gate missed).Proof (affinescript HEAD
58dc2a0, 2026-06-21)compileof ause prelude::{Option,Some,None}consumer goes fromCodegen.UnboundVariable "… Some"to a validout.wasm(V8WebAssembly.compileaccepts it).compilediff over the 30-fileconformance+tests/modulescorpus is identical (OK=16 / FAIL=14 both).dune runtest: 458 tests green, including the new "WASM gen_imports links imported constructors" case.Why a patch, not an affinescript PR
affinescript is out of this session's push scope. The patch + repro + new-issue text are persisted here for a future affinescript-scoped session (or the maintainer) to file the issue and land it. The permanent svalinn/stapeln compiler re-pin waits on the real merged SHA.
Draft — for review of the approach and the persisted artifact.
🤖 Generated with Claude Code
https://claude.ai/code/session_01EsxEhRW4rDbxMo2c9xaa7Z
Generated by Claude Code