diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 1935d55..399e034 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 78ac5d5..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,18 +0,0 @@ -# Changelog - -All notable changes to dafniser 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). - -## [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 (`dafniser.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 db583f6..ce5c13d 100644 --- a/README.adoc +++ b/README.adoc @@ -5,6 +5,8 @@ Jonathan D.A. Jewell :toc: left :icons: font +image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor,link=https://github.com/sponsors/hyperpolymath] + == What Is This? Dafniser generates **correct-by-construction code** for critical functions diff --git a/README.md b/README.md deleted file mode 100644 index 0dd7f59..0000000 --- a/README.md +++ /dev/null @@ -1,122 +0,0 @@ -[![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath) - -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= Dafniser -Jonathan D.A. Jewell -:toc: left -:icons: font - -== What Is This? - -Dafniser generates **correct-by-construction code** for critical functions -using https://dafny.org[Dafny], the verification-aware language created by -Rustan Leino (originally at Microsoft Research). - -Dafny programs carry formal specifications — `requires` / `ensures` clauses, -loop invariants, `decreases` annotations, ghost variables, and lemmas — that -an SMT solver (Z3) proves at compile time. Dafny then compiles the verified -source to C#, Java, Go, Python, or JavaScript. - -Nobody outside research groups writes Dafny by hand. -Dafniser makes verified code generation accessible: -write specifications, get provably correct implementations. - -== How It Works - -[source] ----- -dafniser.toml (specs) ← you write this - │ - ▼ -Spec extraction & validation ← Rust CLI parses pre/postconditions - │ - ▼ -Idris2 ABI meta-proofs ← proves spec consistency (Types, Layout, Foreign) - │ - ▼ -Dafny code generation ← requires/ensures, loop invariants, ghost vars, lemmas - │ - ▼ -Z3 verification ← SMT solver proves every contract - │ - ▼ -Target compilation ← Dafny → C# / Java / Go / Python / JavaScript - │ - ▼ -Zig FFI bridge ← C-ABI integration with your existing codebase ----- - -1. Describe critical functions in `dafniser.toml` with preconditions, postconditions, - and optional invariants. -2. Dafniser generates Dafny source with `requires` / `ensures` contracts, - `decreases` termination measures, ghost variables, and supporting lemmas. -3. Z3 verifies every contract at compile time — if verification fails, - you get a precise counterexample, not a runtime crash. -4. The verified Dafny compiles to your chosen target language. -5. A Zig FFI bridge wraps the compiled output for C-ABI integration. - -== Key Value - -* **Proven-correct code** — Z3 proves every pre/postcondition at compile time -* **Auto-generated from specifications** — no manual Dafny authorship required -* **Multiple output languages** — verified code in C#, Java, Go, Python, JavaScript -* **Formal meta-proofs** — Idris2 dependent types verify spec consistency before codegen -* **Refinement support** — layer abstract specs into concrete implementations with proof - -== Use Cases - -Sorting and searching algorithms:: - Verified implementations of quicksort, binary search, merge sort with - proved bounds and termination. - -Cryptographic primitives:: - Constant-time comparisons, key derivation, hashing wrappers with - proved absence of timing side-channels (within Dafny's model). - -Financial algorithms:: - Interest calculations, rounding, settlement logic with proved - monotonicity and conservation-of-value properties. - -Consensus protocols:: - Leader election, quorum logic, state machine replication steps with - proved safety invariants. - -Safety-critical control logic:: - State machines with proved liveness and deadlock-freedom properties. - -== Dafny Specifics - -Dafniser generates and manages these Dafny constructs: - -* **`requires` / `ensures`** — preconditions and postconditions on every method -* **`decreases`** — termination metrics for recursive functions and loops -* **`invariant`** — loop invariants that hold on every iteration -* **`ghost`** — specification-only variables that vanish at compilation -* **`lemma`** — proof obligations discharged by Z3 to establish complex properties -* **`refines`** — layered module refinement from abstract to concrete - -== Architecture - -Follows the hyperpolymath -iser pattern (same as https://github.com/hyperpolymath/chapeliser[Chapeliser]): - -* **Manifest** (`dafniser.toml`) — declare WHAT you need: function signatures, - preconditions, postconditions, invariants, target language -* **Idris2 ABI** (`src/interface/abi/`) — formal proofs that specifications are - internally consistent (type-safe, non-contradictory, well-scoped) -* **Zig FFI** (`src/interface/ffi/`) — C-ABI bridge to compiled Dafny output -* **Codegen** (`src/codegen/`) — generates Dafny source with full verification annotations -* **Rust CLI** — parses manifest, validates specs, invokes Dafny compiler and Z3 - -User writes zero Dafny. Dafniser generates everything. - -Part of the https://github.com/hyperpolymath/iseriser[-iser family] of acceleration frameworks. - -== Status - -**Pre-alpha / codebase in progress.** Architecture defined, CLI scaffolded, -ABI stubs in place. Dafny codegen and Z3 verification integration pending. - -== License - -SPDX-License-Identifier: MPL-2.0 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()