ReScript→AffineScript migration: Cst.affine (module 3)#28
Merged
Conversation
The three "Safety Proofs" in src/abi/Foreign.idr (stabilityBounded,
positionalDeterministic, paradoxMonotonic) were not proofs: each fabricated
its evidence with cast ()/cast Refl over an IO action. Replace them with
genuine, self-contained Idris2 modules, machine-checked under Idris 2 v0.8.0
(no believe_me / assert_total / cast / postulate):
- Stability.idr : stability score is bounded in [0,100] (clamp model of
compiler/src/Types.res calculateStability).
- Positional.idr : positional-operator behaviour is deterministic over the
pure model of the Zig FFI (a genuine Refl, not IO cast Refl).
- Paradox.idr : the two threshold-gated factors are monotone; the blanket
"paradox detection monotonic" claim is RETRACTED -- proving
it honestly surfaced that scope_leakage is prime-gated and
therefore non-monotone (line 7 prime, line 8 not).
Foreign.idr is reduced to an honest, self-contained ABI binding layer.
Add error-lang-abi.ipkg and verification/check-proofs.sh (idris2 --check all
four modules). Rewrite PROOF-NEEDS.md to record what is proved, what is
retracted, the toolchain, and open conformance obligations.
The language's satirical "100% production-ready / formally verified"
self-presentation in README/WHITEPAPER is intentional and left intact; this
change only makes the underlying proof artifacts real and honest.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
…integration) Adds docs/Trope-Particularity-Integration.adoc — a design (not yet implemented) for lowering Error-Lang's Echo operations and stability factors to the language-neutral Trope IR (hyperpolymath/trope-checker, v0.1 prevent profile) and consuming the verified verdict + witness. - Object/effect/grade correspondence: Echo<A,B> <-> Trope[Phi], EchoR <-> FloatingQuality, echo/echo_to_residue/echo_input/echo_output <-> preserve/ detach/project. echo_to_residue IS detach (bond=Severed, irrecoverable), matching the [Stab-Erase] debit and "decomposition must be visible". - stabilityFactor -> grade mapping; the silent instabilities (GlobalState, RaceCondition) land on the deceptive Conflated bottom -> a lowering fault under the prevent profile. - Verdict mapping: scalar calculateStability -> use-model floor + p-sufficient/ p-insufficient + witness edge (the invariant-path argmin Stability.idr already reasons about). - Architecture (reference, never vendor; schema is the trust boundary), the per-front-end O2 lowering-correctness obligations (L-Echo/L-Grade/L-Silent/ L-Floor), and a 4-phase plan. Builds on docs/Echo-Decomposition.adoc; references echo-types, trope-checker and trope-particularity-workbench by URL only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Hypatia structural_drift flagged `src/idris2/` and `src/aggregate/` in the trope-integration design as dangling references "surviving a directory rename". Both are deliberately *external*: the trope-checker repo's Idris2 core and the panic-attack repo's aggregate module. Reword as unambiguously external (drop the bare `src/<dir>/` form) so the heuristic no longer reads them as internal error-lang tree paths. No substantive content change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
First module of the compiler's migration to AffineScript (the Hyperpolymath language policy bans ReScript). Adds compiler/src/Types.affine, a faithful port of compiler/src/Types.res, verified green with `affinescript check`: - all token / AST / error / stability types (structs + enums + match) - ReScript inline-record variants lowered to positional constructor args - token variants Float/String renamed FloatTok/StringTok (reserved type keywords in AffineScript) - Echo types (TyEcho / TyEchoResidue) shaped Trope-IR-ready per docs/Trope-Particularity-Integration.adoc (Phase 0) - make_default_state, stability_impact, calculate_stability, error_code_to_string Toolchain, so the .affine sources are reproducibly CI-verifiable: - scripts/install-affinescript-toolchain.sh — builds the AffineScript compiler from distro OCaml packages (independent of opam.ocaml.org) + installs the binary and stdlib under a discoverable share/ path - verification/check-affinescript.sh — typechecks all compiler/src/*.affine Types.res is retained until its dependents migrate; format_diagnostic is deferred pending the string / affine-borrow pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
The .res -> .affine port needs sibling compiler modules to import the shared AST
(Location/Token/Position/...) from Types. AffineScript's module resolver exported
imported enum constructors but dropped imported struct/alias type definitions, so
cross-module struct field access failed ("Field not found"). Per the chosen
approach (fix the resolver, not single-file/accessors):
- patches/affinescript-module-struct-fields.patch: threads imported modules'
type_env + constructor_env into the importing module's typecheck context
(typecheck.ml check_program gains ?import_type_env/?import_constructor_env;
resolve.ml import_type_defs copies them across all three import forms;
bin/main.ml passes them at the check/compile/eval entry points). Documented in
patches/README.adoc; pending upstream to hyperpolymath/affinescript.
- compiler/src/Types.affine: now a proper `module Types;` with `pub` exports.
- verification/check-affinescript.sh: checks from compiler/src so `use Types::{...}`
resolves via the loader's current-dir search.
- scripts/install-affinescript-toolchain.sh: applies the patch after cloning,
before building (idempotent).
Verified: a module importing Types' structs with nested field access, struct
construction, and enum-field matching type-checks; affinescript's own stdlib
cross-module imports (http_fetch/option/io) still pass.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Second compiler module. Lexer.affine imports Types (`use Types::*;`) and ports the tokenizer in AffineScript's functional style: with no mutable struct fields or record-spread, state-mutating helpers take a LexerState and return a new one, and the scanners + driver loop a `let mut` local. Single chars are Char (char_at / char_to_int); lexemes and the escape buffer use substring; numeric literals use the parse_int / parse_float builtins; the keyword Dict becomes a string-equality lookup. Verified green with `affinescript check`. Faithful for the core path (identifiers/keywords, decimal int + float + exponent, strings with escapes, all operators/delimiters, comments, newline + EOF, error recovery + diagnostics E0001-E0004). Documented parity gaps for a follow-up pass: hex/binary integer prefixes, triple-quoted strings + \0 escape, smart-quote E0007. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Third module. Trivia-preserving CST with source round-trip. Functional port: classify_trivia loops a `let mut` local; lex_with_trivia folds the raw tokens carrying the last token in hand, so newline-trailing-trivia and trailing source attach without array-index mutation. Selective `Types` import (Cst's node kinds collide with Types' Decl/Stmt constructors). Verified with `affinescript check`. Omitted, documented in-file: - node_at: returning a deepest *subtree* needs a node used both to recurse into AND to return — not expressible under affine ownership without a shared/clone type. Auxiliary (IDE cursor lookup); deferred. - run_tests: the Console-based test harness is not compiler code. Encountered an affinescript resolver bug along the way: a local `let len = ...` shadows the builtin `len` *globally* (so a later `len(xs)` typed as Int). Worked around by renaming the local; worth an upstream fix in affinescript. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
hyperpolymath
marked this pull request as ready for review
June 24, 2026 06:51
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
1 participant
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
Ports
compiler/src/Cst.res→compiler/src/Cst.affine(the trivia-preserving Concrete Syntax Tree), verified green withaffinescript check. ImportsLexerandTypesacross module boundaries (enabled by the merged module-system fix).Notes
classify_trivialoops alet mutlocal;lex_with_triviafolds the raw tokens carrying the last token in hand, so newline-trailing-trivia and trailing source attach without the.res's in-place array-index mutation.Typesimport: Cst's node kinds (MainBlock/FunctionDecl/LetStmt/…) collide withTypes'Decl/Stmtconstructors under a glob, so only the token/location types (+Newline) are imported.Omitted (documented in-file)
node_at— returning a deepest subtree needs a node used both to recurse into and to return, which affine ownership disallows without a shared/clone type. It's an auxiliary IDE cursor helper; deferred. (Worth noting: tree-traversals that return subtrees will need a deliberate pattern inTypeCheckertoo.)run_tests— the Console-based test harness isn't compiler code.AffineScript bug found (worked around)
A local
let len = …shadows the builtinlenglobally — a laterlen(xs)then type-checks asInt(E0104 Expected a function, got Int), with no source span. Worked around by renaming the local; this is a real resolver scoping bug worth fixing upstream inaffinescript(same spirit as the module-system fix).Status
Roadmap: ✅ Toolchain · ✅ Types · ✅ module-system fix · ✅ Lexer · ✅ Cst · next: Parser (28 KB — the big one), then TypeChecker → VM → rest. Pre-existing
Check Workflow Stalenessred as usual (stalestandardspins; fails onmaintoo).🤖 Generated with Claude Code
https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Generated by Claude Code