diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 9e32d15..0395eea 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -30,7 +30,7 @@ jobs: fail-fast: false matrix: include: - - language: javascript-typescript + - language: actions build-mode: none steps: diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index 5528aab..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,30 +0,0 @@ -# Changelog - -All notable changes to iseriser will be documented in this file. - -The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), -and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - -## [Unreleased] - -### Added (2026-05-20) -- `cartridge` subcommand — scaffolds a complete boj-server cartridge skeleton (`-mcp/`) from an `iseriser.toml` manifest. Emits 13 files across `cartridge.json`, `mod.js`, `panels/`, `abi/` (Idris2), `ffi/` (Zig, ADR-0006 5-symbol C ABI), and `adapter/` (unified gated adapter, REST + SSE + GraphQL + gRPC-compat behind the transaction gate). Modelled on the k9iser-mcp pilot (boj-server#73). Implements [standards#89 Phase 2b](https://github.com/hyperpolymath/standards/issues/89). End-to-end verified: `idris2 --build`, `zig build test` on `ffi/` (4/4) and `adapter/` (5/5). (PR #24) - -### Changed (2026-05-20) -- Scaffolder no longer emits `adapter/_adapter.zig` into new -iser repos. The unified transaction-gated adapter belongs to the boj-server cartridge for the -iser (`boj-server/cartridges/-mcp/adapter/`), not to the -iser repo itself. Use the new `cartridge` subcommand to scaffold the cartridge. (PR #23, reverts the wrong-place emission added in #12.) -- Cartridge scaffolder emits `depends = base, contrib` on the generated `.ipkg` to match the pilot convention. (PR #25, corrects an omission in #24.) - -### Added (2026-04-04) -- Criterion benchmark suite (`benches/iseriser_bench.rs`) — 8 benchmarks covering codegen performance and manifest parsing efficiency - -## [0.1.0] - 2026-03-20 - -### Added -- Initial project scaffold from rsr-template-repo -- CLI with subcommands (init, validate, generate, build, run, info) -- Manifest parser (`iseriser.toml`) -- Codegen engine (stubs — target-language-specific implementation pending) -- ABI module (Idris2 proof type definitions) -- Library API for programmatic use -- Full RSR template (17 CI workflows, governance docs, bot directives) -- README.adoc with architecture overview and value proposition diff --git a/Mustfile b/Mustfile new file mode 100644 index 0000000..a864992 --- /dev/null +++ b/Mustfile @@ -0,0 +1,15 @@ +# SPDX-License-Identifier: MPL-2.0 +# Mustfile — hyperpolymath mandatory checks +# See: https://github.com/hyperpolymath/mustfile +# +# Declarative contract of checks that MUST pass. Each maps to a recipe +# that already exists in this repo's Justfile. +version: 1 + +checks: + - name: security + run: just lint + - name: tests + run: just test + - name: format + run: just fmt diff --git a/README.adoc b/README.adoc index 1bc63fa..234b83c 100644 --- a/README.adoc +++ b/README.adoc @@ -22,6 +22,20 @@ image:https://img.shields.io/badge/FFI-Zig-orange[Zig FFI] ''' +[TIP] +==== +**New here? Start with the coordination layer:** + +* link:docs/ATLAS.adoc[**The -iser Atlas**] — route a need straight to the right + -iser ("I want to… → use…"). +* link:docs/theory/AOLD.adoc[**Aspect-Oriented Language Design**] — the design + philosophy (each language's superpower as a bolt-on _aspect_; the "mech suit" + model; why this is the _dual_ of aggregate-library). +* link:docs/theory/iSOS.adoc[**Integrated Stack of Stacks**] — how aspects + _compose_ over one shared Idris2-ABI/Zig-FFI seam, kept honest by + invariant-path. +==== + == What is the -iser Pattern? An **-iser** is a Rust CLI that bridges the gap between a _specialist language_ diff --git a/docs/ATLAS.adoc b/docs/ATLAS.adoc new file mode 100644 index 0000000..d115b58 --- /dev/null +++ b/docs/ATLAS.adoc @@ -0,0 +1,120 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += The -iser Atlas — find the right -iser +Jonathan D.A. Jewell +:toc: left +:toclevels: 2 +:icons: font +:url-org: https://github.com/hyperpolymath + +[.lead] +**This is the map.** If you have a codebase and a need, this page routes you to +the -iser that grants it — the "right place" index for the augmentation family. +It is the coordination layer for Aspect-Oriented Language Design (see +`theory/AOLD.adoc`) and the Integrated Stack of Stacks (`theory/iSOS.adoc`). + +== How to read this + +Every -iser injects _one_ specialist language's superpower into the code you +already have, via `manifest → Idris2 ABI → Zig FFI → codegen → build/run`. You +do not learn the language. Find your need in the left column; go to the -iser in +the middle. + +== Route by need + +[cols="3,2,3",options="header"] +|=== +| I want to… | Use | Aspect / language essence + +| …distribute a single-machine workload across a cluster | {url-org}/chapeliser[chapeliser] | Chapel data-parallelism +| …push array/number crunching onto the GPU | {url-org}/futharkiser[futharkiser] | Futhark kernels +| …make a Python/R pipeline ~100× faster | {url-org}/julianiser[julianiser] | Julia +| …add fault tolerance / supervision to concurrent code | {url-org}/otpiser[otpiser] | OTP/BEAM +| …get data-race freedom for concurrency | {url-org}/ponyiser[ponyiser] | Pony reference capabilities +| …optimise an image/video pipeline | {url-org}/halideiser[halideiser] | Halide schedules +| …rewrite array patterns as optimised primitives | {url-org}/bqniser[bqniser] | BQN +| …generate high-performance C libraries | {url-org}/nimiser[nimiser] | Nim metaprogramming +| …prove critical functions correct-by-construction | {url-org}/dafniser[dafniser] | Dafny +| …model-check a state machine | {url-org}/tlaiser[tlaiser] | TLA+/PlusCal +| …find counterexamples in an API model | {url-org}/alloyiser[alloyiser] | Alloy +| …get proven-correct wrappers from interfaces | {url-org}/idrisiser[idrisiser] | Idris2 dependent types +| …verify real-time embedded logic | {url-org}/lustreiser[lustreiser] | Lustre +| …add formal type safety to a query language | {url-org}/typedqliser[typedqliser] | graded type systems +| …wrap C in zero-cost memory safety | {url-org}/atsiser[atsiser] | ATS linear types +| …enforce use-exactly-once on resources | {url-org}/ephapaxiser[ephapaxiser] | Ephapax linear semantics +| …target WASM with affine + dependent types | {url-org}/affinescriptiser[affinescriptiser] | AffineScript +| …augment any database (drift/provenance/temporal) | {url-org}/verisimiser[verisimiser] | VeriSimDB octad +| …make configs self-validating | {url-org}/k9iser[k9iser] | K9 contracts +| …add cryptographic attestation to markup/config | {url-org}/a2mliser[a2mliser] | A2ML +| …make operations reversible + auditable | {url-org}/oblibeniser[oblibeniser] | Oblíbený +| …add energy/carbon/cost awareness | {url-org}/eclexiaiser[eclexiaiser] | Eclexia +| …put provably-safe ethical guardrails on an AI agent | {url-org}/phronesiser[phronesiser] | Phronesis +| …add consent flows + accessibility | {url-org}/wokelangiser[wokelangiser] | WokeLang +| …model uncertainty over deterministic code | {url-org}/betlangiser[betlangiser] | Betlang ternary probability +| …expose a complex API progressively | {url-org}/mylangiser[mylangiser] | My-Lang +| …formalise ISU figure-skating notation | {url-org}/anvomidaviser[anvomidaviser] | Anvomidav +| …scaffold a brand-new -iser for another language | {url-org}/iseriser[iseriser] | the meta-framework +|=== + +NOTE: Status across the family is _scaffold → pre-alpha_; `chapeliser`, +`verisimiser`, and `typedqliser` are the most developed. Each -iser's own +`ROADMAP.adoc` is the source of truth for its maturity. (The family READMEs +historically over-stated test counts; trust the per-repo `cargo test` output.) + +== What -iserisation is — and is not + +[cols="1,3",options="header"] +|=== +| -iserisation is… | …and it is _not_ + +| **augmentation**: bolt one specialist language's power onto a foreign host +| **aggregate-library**: aLib is the _dual_ — the minimal _overlap_ common to all + systems. -isers add the exotic edge; aLib distils the shared core. + +| a **coordination atlas**: the index that sends you to the right capability +| nextgen-language-evangeliser: that advocates adopting whole next-gen languages; + the atlas routes you to a _capability_, no adoption required. + +| a family of **proof-carrying seams** (Idris2 ABI + Zig FFI) +| the dyadic language/toolchain design of Ephapax, or an AffineScript "face". +|=== + +== The pattern in one diagram + +[literal] +.... + your app ──► .toml ──► the -iser CLI + │ + ┌─────────────────┼─────────────────┐ + ▼ ▼ ▼ + Idris2 ABI Zig FFI target codegen + (prove interface) (C-ABI bridge) (specialist lang) + └─────────────────┴─────────────────┘ + ▼ + your app, now wearing the aspect +.... + +== Getting started + +[source,bash] +---- +# install any -iser (standalone Rust binary) +cargo install chapeliser # …or any name above + +# the shared five-command interface + init # write a manifest for your project + validate # check it against the Idris2 ABI spec + generate # emit the specialist-language code + build # build the generated output + run # run it +---- + +To create an aspect for a language that has no -iser yet, use the meta-framework: +`iseriser generate -m .toml -o ./iser` (see +`examples/newlang/iseriser.toml`). + +== See also + +* `theory/AOLD.adoc` — the design philosophy (languages as aspects). +* `theory/iSOS.adoc` — the architecture (composing aspects). +* `../README.adoc` — family overview, architecture diagram, full install/usage. diff --git a/docs/theory/AOLD.adoc b/docs/theory/AOLD.adoc new file mode 100644 index 0000000..6025544 --- /dev/null +++ b/docs/theory/AOLD.adoc @@ -0,0 +1,153 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Aspect-Oriented Language Design (AOLD) +Jonathan D.A. Jewell +:toc: left +:toclevels: 3 +:icons: font + +[.lead] +**AOLD is the design philosophy behind the -iser family.** Instead of choosing +one general-purpose language and living with its global trade-offs, AOLD treats +each specialist language's _unique strength_ as a weavable **aspect** that you +can bolt onto an existing codebase on demand — and remove just as easily. + +== The problem AOLD answers + +Every language makes one global bet. Chapel bets everything on distributed +data-parallelism; Pony on data-race-free actors; Dafny on +correct-by-construction proof; Futhark on GPU array kernels; OTP on +fault-tolerant supervision. Each is _extraordinary_ at its one thing and +ordinary (or absent) at everything else. + +In practice that bet is hard to take: + +. **Steep learning curve** — to get the superpower you must rewrite in, or deeply + learn, the specialist language. +. **All-or-nothing adoption** — there is rarely an incremental path; you commit + the whole system or none of it. +. **Integration tax** — wiring the specialist runtime into your existing + Rust/C/Zig project is non-trivial and easy to get subtly wrong. + +So the superpowers stay locked behind their languages, and most projects never +touch them. + +== The core idea: languages as aspects + +AOLD unlocks the superpower _without_ taking the global bet. An **-iser** is a +Rust CLI that injects exactly one specialist language's capability into the code +you already write, through a uniform, proof-carrying pipeline: + +[literal] +.... + your manifest ──► Idris2 ABI ──► Zig FFI ──► target-language codegen ──► build / run + (what you want) (prove the (C-ABI (emit the specialist (you never + interface) bridge) language's code) wrote any) +.... + +You describe _what_ you want in a declarative TOML manifest. The -iser validates +it against a formally verified **Idris2 ABI**, bridges to your application across +a **Zig FFI** seam, generates the specialist-language code, and builds it. You +get the aspect; you never learn the language. + +== The "mech suit" mental model + +The cleanest way to think about an -iser is as a **mech suit for your +application**. Your program/database/tool stays exactly what it is — its own +language, its own logic. The -iser is an _exoskeleton_ that grants it one exotic +capability it did not have: distribution, GPU acceleration, data-race freedom, +fault tolerance, machine-checked correctness, energy-awareness, reversibility. + +Three properties make it a suit rather than a rewrite: + +* **Addable** — you bolt it on around the existing code, at the boundary. +* **Removable / reversible** — take the suit off and the original program is + unchanged. Nothing is load-bearing on the aspect that cannot be unwound. +* **Composable** — suits stack. See `iSOS.adoc` for how multiple aspects layer + on one host (the _Integrated Stack of Stacks_). + +== What AOLD is _not_ + +[cols="1,3",options="header"] +|=== +| It is not… | …because + +| aggregate-library (aLib) +| aLib is the **dual** of AOLD. aLib finds the minimal _overlap_ common to all + systems (subtractive: the greatest common denominator, conformance-tested). + AOLD adds the exotic _differentiator_ of one system (additive: the specialist + edge). aLib reduces to the shared core; -isers extend with the rare capability. + +| the dyadic toolchain/language design of Ephapax +| Ephapax is about the design of a single language and its paired toolchain. + AOLD is about _weaving many languages' aspects_ onto a foreign host. + +| an AffineScript-style "face" +| A "face" is a uniform surface over a substrate. An aspect is a _capability + injection_ at a proof-carrying seam, not a presentation layer. + +| nextgen-language-evangeliser +| That project advocates for next-generation languages as wholes. The -iser + atlas (`ATLAS.adoc`) routes you to a _capability_, not to a language to adopt. +|=== + +== The aspect taxonomy + +Each -iser is one aspect. The family is the palette. + +[cols="2,3,2",options="header"] +|=== +| -iser | Aspect (the superpower it weaves in) | Host gains + +| typedqliser | Formal type safety (10 graded levels) over a query language | injection-/null-/schema-safe queries +| chapeliser | Chapel distributed data-parallelism | single-machine workload → cluster +| verisimiser | VeriSimDB octad capabilities | drift / provenance / temporal over any DB +| julianiser | Julia numerical performance | 100× speedups for Python/R pipelines +| futharkiser | Futhark GPU array kernels | data-parallel ops → GPU +| idrisiser | Idris2 dependent-type proofs | proven-correct wrappers from interfaces +| dafniser | Dafny correct-by-construction | verified critical functions +| tlaiser | TLA+/PlusCal model checking | state machines checked for safety/liveness +| alloyiser | Alloy relational model finding | formal models from API specs +| lustreiser | Lustre synchronous dataflow | verified real-time embedded code +| ponyiser | Pony reference capabilities | data-race freedom for concurrent code +| otpiser | OTP/BEAM supervision | fault-tolerance trees, let-it-crash resilience +| halideiser | Halide schedule optimisation | optimised image/video pipelines +| bqniser | BQN array primitives | array patterns rewritten as optimised idioms +| nimiser | Nim metaprogramming | high-performance C libraries +| atsiser | ATS linear types | zero-cost memory safety wrapping C +| affinescriptiser | AffineScript affine + dependent types | WASM-targeted resource safety +| a2mliser | A2ML cryptographic attestation | tamper-evident markup / configuration +| ephapaxiser | Ephapax single-use linear semantics | enforce use-exactly-once on resources +| eclexiaiser | Eclexia cost modelling | energy / carbon / resource-cost awareness +| k9iser | K9 contracts | configs become self-validating +| oblibeniser | Oblíbený reversibility | operations made reversible + auditable +| phronesiser | Phronesis ethical constraints | provably-safe guardrails for AI agents +| wokelangiser | WokeLang consent + a11y patterns | consent flows and accessibility +| betlangiser | Betlang ternary probabilistic modelling | uncertainty over deterministic code +| mylangiser | My-Lang progressive disclosure | layered interfaces over complex APIs +| anvomidaviser | Anvomidav ISU notation | figure-skating programs as formal artefacts +|=== + +`iseriser` is the meta-framework that scaffolds new aspects into this palette. + +== The proof-carrying seam + +An aspect is only worth bolting on if its guarantee survives the journey into +your host. AOLD makes that survivable by construction: + +* The **Idris2 ABI** is where the aspect's invariant is _proven_ — e.g. + chapeliser proves `PartitionComplete` (every item is placed) and + `PartitionDisjoint` (no item is placed twice) and `GatherConservation` + (no result is lost). +* The **Zig FFI** is the zero-overhead C-ABI bridge that carries data across the + boundary without re-introducing unsafety. +* **invariant-path** is the conscience: it _traces the proven invariant across + the seam into the host_ and flags any point where the guarantee is silently + over-generalised (the classic `theorem → guarantee → "universal claim"` + slide). See `iSOS.adoc`. + +== See also + +* `iSOS.adoc` — how aspects compose into an Integrated Stack of Stacks. +* `../ATLAS.adoc` — the routing map: pick the -iser for your need. +* `../../README.adoc` — the family overview and install/usage. diff --git a/docs/theory/iSOS.adoc b/docs/theory/iSOS.adoc new file mode 100644 index 0000000..57d6a64 --- /dev/null +++ b/docs/theory/iSOS.adoc @@ -0,0 +1,101 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += iSOS — the Integrated Stack of Stacks +Jonathan D.A. Jewell +:toc: left +:toclevels: 3 +:icons: font + +[.lead] +**iSOS is the architecture that lets AOLD aspects compose.** Where `AOLD.adoc` +explains _why_ each specialist language becomes a bolt-on aspect, iSOS explains +_how_ the aspects fit together: every -iser is a self-contained stack, and +because they all speak one shared contract, they compose into a +**stack of stacks**. + +== One contract, many stacks + +Each -iser is a complete vertical stack: + +[literal] +.... + specialist language (Chapel, Futhark, Pony, Dafny, OTP, …) + ▲ + target-language codegen + ▲ + Zig FFI ── C-ABI bridge + ▲ + Idris2 ABI ── formal proof of the interface + ▲ + manifest ── the declarative "what" +.... + +The stacks differ wildly at the top (the specialist language) but are +_identical at the seam_: every -iser exposes its capability across the same +**Idris2-ABI + Zig-FFI** contract. That shared seam is what makes them +composable rather than 28 unrelated tools. + +== Why the seam is the whole game + +A general-purpose language forces a single global ABI/runtime; you cannot graft +another language's runtime on without a foreign-function minefield. iSOS inverts +this: the ABI is _specified and proven_ in Idris2, and _bridged_ in Zig, so any +host that can call C can host any aspect — and any two aspects can sit on the +same host without knowing about each other. + +* **Idris2 owns the ABI.** Dependent types pin down memory layout, calling + convention, and the aspect's invariants as compile-time obligations. +* **Zig owns the FFI.** A zero-overhead, memory-safe C-ABI bridge with built-in + cross-compilation and no runtime dependency. +* The host owns _nothing it didn't already own_. The aspect is additive. + +== invariant-path: the conscience of the stack + +Composing proofs is where guarantees usually die. A theorem proved _inside_ an +aspect (`PartitionDisjoint` holds for the Chapel partition) is easy to quietly +restate, one boundary later, as a universal claim it never earned ("the pipeline +is correct"). That illegitimate strengthening — + +[literal] +.... + theorem → guarantee → "general truth" + local result → universal claim + assumption-bound result → unconditional fact +.... + +— is exactly what **invariant-path** is built to catch. It is a _claim-path +debugger_, not a truth engine: it traces how a claim travels from its source +(the Idris2 proof) to where it is relied upon (the host call site), and flags +each point where the invariant is carried further than it was proved. In iSOS, +invariant-path is how you keep a _stack of_ proofs honest when no single proof +spans the whole tower. + +== Composing aspects — stacking mech suits + +Because the seam is uniform, aspects layer. Two worked patterns from the estate: + +* **boj-server (Box of Justice).** A server whose core correctness is _proven_ in + Idris2, then extended across the Zig seam to graft on **OTP/BEAM scalability** + (the otpiser-style aspect) — fault-tolerant concurrency added to a proven core + _without rewriting_ it. Proof at the bottom, resilience bolted on top. +* **panic-attacker → chapeliser.** A high-rigor static-analysis + dynamic-attack + tool whose "mass-panic" mode is **chapelised** to distribute analysis across a + cluster — the same host gaining a distribution aspect on demand. + +The general shape — _a proven core, augmented with an esoteric language's power +through a proof-carrying seam_ — recurs. iSOS is the recognition that this shape +generalises, and the -iser family is its systematic build-out. + +== Relationship to the rest of the estate + +* **AOLD** (`AOLD.adoc`) — the philosophy; aspects as the unit of design. +* **iSOS** (this doc) — the architecture; the shared seam that composes them. +* **aggregate-library** — the _dual_: the minimal overlap _common_ to all + systems, not the specialist edge of one. iSOS adds; aLib intersects. +* **rsr-template `src/aspects/`** — the structural "Aspects Pillar" every RSR repo + carries, where a host project declares which aspects it wears. + +== See also + +* `AOLD.adoc` — the design philosophy and the aspect taxonomy. +* `../ATLAS.adoc` — route a need to the right aspect. diff --git a/examples/SafeDOMExample.affine b/examples/SafeDOMExample.affine new file mode 100644 index 0000000..2a62c1d --- /dev/null +++ b/examples/SafeDOMExample.affine @@ -0,0 +1,129 @@ +// SPDX-License-Identifier: MPL-2.0 +// SafeDOMExample.affine — formally-verified DOM mounting (aspirational). +// +// This example shows the *shape* of SafeDOM consumer code in current +// AffineScript syntax. The `SafeDOM` stdlib surface it references +// (`mount_safe`, `mount_when_ready`, `mount_batch`, +// `proven_selector_validate`, `proven_html_validate`, `mount`) is the +// target of `affinescript#56` (DOM+Pixi binding survey) and does not +// yet exist in the published stdlib. The file is therefore +// parse-checked but not type-checked end-to-end until #56 lands the +// bindings; `affinescript check` reports `Resolve.UndefinedModule +// SafeDOM` which is expected. +// +// Previous versions of this file (estate-wide, 5 dialect variants) +// pre-dated ADR-014 (qualified paths), ADR-016 (effect rows), and the +// `#{`-record-literal sigil (ADR-215). They were retired in favour of +// this canonical via the gitbot-fleet#208 sweep (2026-05-26). + +module SafeDOMExample; + +use prelude::{Option, Some, None, Result, Ok, Err}; + +// `Element` and friends are nominal extern types for now — the real +// shape lands with affinescript#56. +extern type Element; +extern type Selector; +extern type ValidHTML; + +// Single-mount status, lifted from the host into a typed tag union. +enum MountStatus { + Mounted(Element), + MountPointNotFound(String), + InvalidSelector(String), + InvalidHTML(String) +} + +// Batch-mount result. +enum MountResult { + Mounted([Element]), + Failed(String) +} + +// Spec for one element in a batch mount. +struct MountSpec { + selector: String, + html: String +} + +// SafeDOM's host-side surface, all IO-effecting. Callbacks are passed +// as separate parameters (rather than a `MountCallbacks` record) +// because fn-typed struct fields are not currently parser-supported. +extern fn mount_safe( + selector: ref String, + html: ref String, + on_success: fn(Element) -> (), + on_error: fn(String) -> (), +) -{IO}-> (); + +extern fn mount_when_ready( + selector: ref String, + html: ref String, + on_success: fn(Element) -> (), + on_error: fn(String) -> (), +) -{IO}-> (); + +extern fn mount_batch(specs: ref [MountSpec]) -{IO}-> MountResult; + +extern fn proven_selector_validate(s: ref String) -{IO}-> Result; +extern fn proven_html_validate(s: ref String) -{IO}-> Result; +extern fn mount(sel: ref Selector, html: ref ValidHTML) -{IO}-> MountStatus; + +extern fn array_for_each(xs: ref [Element], f: fn(Element) -> ()) -{IO}-> (); +extern fn array_len(xs: ref [Element]) -> Int; + +// Example 1 — basic mount with success/error branches. +pub fn mount_app() -{IO}-> () { + mount_safe( + "#app", + "

Hello, World!

Mounted safely with proofs.

", + fn(el) -> () { Console::log("App mounted successfully"); }, + fn(err) -> () { Console::error("Mount failed: " ++ err); }, + ); +} + +// Example 2 — defer until DOM ready. +pub fn mount_when_dom_ready() -{IO}-> () { + mount_when_ready( + "#app", + "

App Title

", + fn(_el) -> () { Console::log("Mounted after DOM ready"); }, + fn(err) -> () { Console::error("Failed: " ++ err); }, + ); +} + +// Example 3 — atomic batch mount. +pub fn mount_multiple() -{IO}-> () { + let specs = [ + MountSpec #{ selector: "#header", html: "

Site Title

" }, + MountSpec #{ selector: "#nav", html: "" }, + MountSpec #{ selector: "#main", html: "

Content here

" }, + MountSpec #{ selector: "#footer", html: "
2026
" }, + ]; + + match mount_batch(specs) { + Mounted(elements) => { + Console::log("Batch mount succeeded"); + array_for_each(elements, fn(_el) -> () { Console::log(" element"); }); + }, + Failed(err) => { + Console::error("Batch mount failed (atomic — none mounted): " ++ err); + } + } +} + +// Example 4 — explicit two-stage validation before mounting. +pub fn mount_with_validation() -{IO}-> () { + match proven_selector_validate("#my-app") { + Err(e) => Console::error("Invalid selector: " ++ e), + Ok(valid_selector) => match proven_html_validate("
Content
") { + Err(e) => Console::error("Invalid HTML: " ++ e), + Ok(valid_html) => match mount(valid_selector, valid_html) { + Mounted(_el) => Console::log("Mounted with validated inputs"), + MountPointNotFound(s) => Console::error("Element not found: " ++ s), + InvalidSelector(_) => Console::error("impossible — already validated"), + InvalidHTML(_) => Console::error("impossible — already validated"), + }, + }, + } +} diff --git a/examples/SafeDOMExample.res b/examples/SafeDOMExample.res deleted file mode 100644 index e5c9046..0000000 --- a/examples/SafeDOMExample.res +++ /dev/null @@ -1,109 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Example: Using SafeDOM for formally verified DOM mounting - -open SafeDOM - -// Example 1: Basic mounting with error handling -let mountApp = () => { - mountSafe( - "#app", - "

Hello, World!

Mounted safely with proofs.

", - ~onSuccess=el => { - Console.log("✓ App mounted successfully!") - Console.log("Element:", el) - }, - ~onError=err => { - Console.error("✗ Mount failed:", err) - } - ) -} - -// Example 2: Wait for DOM ready before mounting -let mountWhenDOMReady = () => { - mountWhenReady( - "#app", - "

App Title

", - ~onSuccess=_ => Console.log("✓ Mounted after DOM ready"), - ~onError=err => Console.error("✗ Failed:", err) - ) -} - -// Example 3: Batch mounting (atomic - all or nothing) -let mountMultiple = () => { - let specs = [ - {selector: "#header", html: "

Site Title

"}, - {selector: "#nav", html: ""}, - {selector: "#main", html: "

Content here

"}, - {selector: "#footer", html: "
© 2026
"} - ] - - switch mountBatch(specs) { - | Ok(elements) => { - Console.log(`✓ Successfully mounted ${Array.length(elements)} elements`) - elements->Array.forEach(el => Console.log(" -", el)) - } - | Error(err) => { - Console.error("✗ Batch mount failed:", err) - Console.error(" (None were mounted - atomic operation)") - } - } -} - -// Example 4: Explicit validation before mounting -let mountWithValidation = () => { - // Validate selector first - switch ProvenSelector.validate("#my-app") { - | Error(e) => Console.error(`Invalid selector: ${e}`) - | Ok(validSelector) => { - // Validate HTML - switch ProvenHTML.validate("
Content
") { - | Error(e) => Console.error(`Invalid HTML: ${e}`) - | Ok(validHtml) => { - // Now mount with proven safety - switch mount(validSelector, validHtml) { - | Mounted(el) => Console.log("✓ Mounted with validated inputs:", el) - | MountPointNotFound(s) => Console.error(`✗ Element not found: ${s}`) - | InvalidSelector(_) => Console.error("Impossible - already validated") - | InvalidHTML(_) => Console.error("Impossible - already validated") - } - } - } - } -} - -// Example 5: Integration with TEA -module MyApp = { - type model = {message: string} - type msg = NoOp - - let init = () => {message: "Hello from TEA"} - let update = (model, _msg) => model - let view = model => `

${model.message}

` -} - -let mountTEAApp = () => { - let model = MyApp.init() - let html = MyApp.view(model) - - mountWhenReady( - "#tea-app", - html, - ~onSuccess=el => { - Console.log("✓ TEA app mounted") - // Set up event handlers, subscriptions here - }, - ~onError=err => Console.error(`✗ TEA mount failed: ${err}`) - ) -} - -// Entry point -let main = () => { - Console.log("SafeDOM Examples") - Console.log("================\n") - - // Choose which example to run - mountWhenDOMReady() // Run on DOM ready -} - -// Auto-execute when module loads -main() diff --git a/src/codegen/scaffold.rs b/src/codegen/scaffold.rs index e3d2c7d..ba3e478 100644 --- a/src/codegen/scaffold.rs +++ b/src/codegen/scaffold.rs @@ -66,6 +66,7 @@ pub fn scaffold_repo(manifest: &Manifest, output_dir: &Path) -> ScaffoldResult { files.push(generate_license()); files.push(generate_gitignore()); files.push(generate_editorconfig()); + files.push(generate_mustfile()); // Apply language-specific customizations customizer::apply_customizations(&model, &mut files); @@ -1071,6 +1072,33 @@ Thumbs.db } } +/// Generate the root `Mustfile` — the RSR-mandatory declarative contract of +/// checks that MUST pass. Each check maps to a recipe emitted in the Justfile, +/// so a freshly scaffolded repo is born standards-compliant (REQUIRED-FILES.adoc). +fn generate_mustfile() -> GeneratedFile { + let content = r#"# SPDX-License-Identifier: MPL-2.0 +# Mustfile — hyperpolymath mandatory checks +# See: https://github.com/hyperpolymath/mustfile +# +# Declarative contract of checks that MUST pass. Each maps to a recipe +# that already exists in this repo's Justfile. +version: 1 + +checks: + - name: security + run: just lint + - name: tests + run: just test + - name: format + run: just fmt +"# + .to_string(); + GeneratedFile { + path: PathBuf::from("Mustfile"), + content, + } +} + /// Generate `.editorconfig`. fn generate_editorconfig() -> GeneratedFile { let content = r#"# EditorConfig — generated by iseriser