diff --git a/site/.gitignore b/site/.gitignore index 449e24e3..695208b2 100644 --- a/site/.gitignore +++ b/site/.gitignore @@ -1,7 +1,6 @@ node_modules dist .astro -src/content/docs/index.md src/content/docs/getting-started.md src/content/docs/spec.md src/content/docs/spec-dafny.md @@ -10,4 +9,6 @@ src/content/docs/tools.md src/content/docs/design.md src/content/docs/architecture-narrowing.md src/content/docs/agents.md +src/content/docs/subset.md +src/content/docs/case-studies.md src/content/docs/howto_greenfield.md diff --git a/site/astro.config.mjs b/site/astro.config.mjs index a5eb84af..355e4bb1 100644 --- a/site/astro.config.mjs +++ b/site/astro.config.mjs @@ -48,17 +48,17 @@ function rehypeRepoLinks() { // only touch links whose visible text IS a bare *.md filename, so intentional // text like `[SPEC.md §2]` or `[TOOLS.md#narrow-rules]` is left untouched. const LINK_NAMES = { - "/": "Overview", - "/subset/": "Overview (Subset)", - "/getting-started/": "Getting Started", - "/howto_greenfield/": "Greenfield tutorial", + "/case-studies/": "Case studies & examples", + "/subset/": "Supported TypeScript subset", + "/getting-started/": "Getting started in an existing codebase", + "/howto_greenfield/": "Start a new project", "/spec/": "Specification", "/spec-dafny/": "Dafny backend spec", "/spec-lean/": "Lean backend spec", - "/tools/": "Tools", + "/tools/": "Toolchain architecture", "/design/": "Design", "/architecture-narrowing/": "Narrowing architecture", - "/agents/": "Agents", + "/agents/": "Guidance for agents", } const BARE_FILENAME = /^[A-Za-z0-9_]+\.md$/ @@ -91,11 +91,12 @@ export default defineConfig({ social: [{ icon: "github", label: "GitHub", href: "https://github.com/midspiral/LemmaScript" }], sidebar: [ { - label: "Getting started", + label: "Start here", items: [ - { label: "Overview (Subset)", link: "/subset/" }, - { label: "Overview (Brownfield)", link: "/getting-started/" }, - { label: "Howto (Greenfield)", link: "/howto_greenfield/" }, + { label: "What is LemmaScript?", link: "/" }, + { label: "Installation", link: "/installation/" }, + { label: "How the loop works", link: "/how-the-loop-works/" }, + { label: "How to: Brownfield", link: "/getting-started/" }, ], }, { @@ -117,22 +118,25 @@ export default defineConfig({ ], }, { - label: "Specification", + label: "Reference", items: [ - { label: "Overview", link: "/spec/" }, + { label: "CLI (lsc)", link: "/reference/cli/" }, + { label: "Supported TypeScript subset", link: "/subset/" }, + { label: "Specification", link: "/spec/" }, { label: "Dafny backend", link: "/spec-dafny/" }, { label: "Lean backend", link: "/spec-lean/" }, ], }, - { label: "Tools", link: "/tools/" }, { - label: "Design", + label: "Under the hood", items: [ { label: "Design rationale", link: "/design/" }, + { label: "Toolchain architecture", link: "/tools/" }, { label: "Architecture: narrowing", link: "/architecture-narrowing/" }, + { label: "Guidance for agents", link: "/agents/" }, + { label: "Case studies & examples", link: "/case-studies/" }, ], }, - { label: "Agents", link: "/agents/" }, ], }), ], diff --git a/site/scripts/sync-docs.mjs b/site/scripts/sync-docs.mjs index 93dab60d..de03ac37 100644 --- a/site/scripts/sync-docs.mjs +++ b/site/scripts/sync-docs.mjs @@ -12,24 +12,28 @@ const here = dirname(fileURLToPath(import.meta.url)) const ROOT = join(here, "..", "..") // repo root: site/scripts -> site -> repo const OUT = join(here, "..", "src", "content", "docs") -// Which root docs become site pages. +// Which root docs become site pages. `title` (optional) overrides the H1-derived +// page title so synced pages can carry reader-facing names without editing the +// repo files themselves. const DOCS = [ - { src: "README.md", out: "index.md" }, // home / overview + // The site homepage (index.md) is hand-written; the README syncs to its own + // page under "Under the hood" as the case-studies/overview reference. + { src: "README.md", out: "case-studies.md", title: "Case studies & examples" }, { src: "SUBSET.md", out: "subset.md" }, - { src: "GETTING_STARTED.md", out: "getting-started.md" }, + { src: "GETTING_STARTED.md", out: "getting-started.md", title: "Getting started in an existing codebase" }, { src: "TUTORIAL_GREENFIELD.md", out: "howto_greenfield.md" }, { src: "SPEC.md", out: "spec.md" }, { src: "SPEC_DAFNY.md", out: "spec-dafny.md" }, { src: "SPEC_LEAN.md", out: "spec-lean.md" }, - { src: "TOOLS.md", out: "tools.md" }, + { src: "TOOLS.md", out: "tools.md", title: "Toolchain architecture" }, { src: "DESIGN.md", out: "design.md" }, { src: "ARCHITECTURE_NARROWING.md", out: "architecture-narrowing.md" }, - { src: "AGENTS.md", out: "agents.md" }, + { src: "AGENTS.md", out: "agents.md", title: "Guidance for agents" }, ] // filename -> site route, for rewriting cross-doc links so site nav works. const ROUTES = { - "README.md": "/", + "README.md": "/case-studies/", "SUBSET.md": "/subset/", "GETTING_STARTED.md": "/getting-started/", "TUTORIAL_GREENFIELD.md": "/howto_greenfield/", @@ -94,14 +98,14 @@ for (const d of DOCS) rmSync(join(OUT, d.out), { force: true }) mkdirSync(OUT, { recursive: true }) const broken = [] -for (const { src, out } of DOCS) { +for (const { src, out, title: override } of DOCS) { const raw = readFileSync(join(ROOT, src), "utf8") const { title, body } = titleAndBody(raw) const rewritten = rewriteLinks(body) broken.push(...missingRepoLinks(src, rewritten)) const target = join(OUT, out) mkdirSync(dirname(target), { recursive: true }) - writeFileSync(target, `---\ntitle: "${esc(title)}"\n---\n\n${rewritten}`) + writeFileSync(target, `---\ntitle: "${esc(override ?? title)}"\n---\n\n${rewritten}`) } if (broken.length) { diff --git a/site/src/content/docs/how-the-loop-works.md b/site/src/content/docs/how-the-loop-works.md new file mode 100644 index 00000000..2e1b36dd --- /dev/null +++ b/site/src/content/docs/how-the-loop-works.md @@ -0,0 +1,66 @@ +--- +title: "How the loop works" +description: "Contracts, checks, and iteration — the concepts behind LemmaScript in five minutes, no setup required." +--- + + + +Four ideas explain almost everything else in these docs. + +## 1. A contract is the function's API for correctness + +Above a function, `//@ ` annotations state what it needs and what it promises: + +```typescript +//@ contract Never lets the charge exceed the available balance. +//@ requires balance >= 0 +//@ requires amount >= 0 +//@ ensures amount <= balance ==> \result === balance - amount +//@ ensures amount > balance ==> \result === 0 +function charge(balance: number, amount: number): number { /* … */ } +``` + +- `requires` — what callers must guarantee coming in +- `ensures` — what the function guarantees going out (`\result` is the return value) +- `contract` — the same promise in plain English, for the human reviewer + +These are the three you'll see most. The full annotation list is in +[the specification](/spec/#2-the---annotation-language). + +The implementation stays ordinary TypeScript. Contracts are comments, so they cost +nothing at runtime and change nothing about how the code builds or ships. + +## 2. `lsc check` decides, it doesn't sample + +Testing runs the code on chosen inputs; `lsc check` translates the function and its +contract to a prover (Dafny by default) and asks whether the implementation meets +the spec **for every input the contract admits**. The answer is a verdict, not a +survey: correct, or not correct yet — with the failing obligation to point at. + +The two do different jobs, and both matter: contracts settle the core logic; +tests remain the right tool for integration, I/O, and everything outside the +verified boundary. + +## 3. "Not correct yet" is a loop state, not a bug report + +When a check fails, either the code doesn't do what the contract says, or the +contract doesn't say what you meant. The loop is: adjust one of them, re-run, +repeat. Agents drive this loop well — with the +[skills](https://github.com/midspiral/lemmascript-skills) installed, an agent writes the contract and the code +together and iterates until the check passes, so what surfaces is correct code. +Your job shifts to reviewing the contract: a few declarative lines that say +exactly what was guaranteed. + +## 4. Generated files carry the proof work + +For the Dafny backend, `lsc` writes two files next to your source: `foo.dfy.gen` +(always regeneratable — never edit) and `foo.dfy` (yours — helper lemmas and proof +additions accumulate here; the difference from `.dfy.gen` must be additions-only, +and `lsc check` enforces that). After editing the TypeScript, `lsc regen` +three-way-merges the new generated code into `foo.dfy` so proof work is never lost. +Precise rules live in the [Dafny backend spec](/spec-dafny/). + +## Next + +- [What TypeScript is supported](/subset/) — the subset the prover understands +- [CLI reference](/reference/cli/) — every command in the loop diff --git a/site/src/content/docs/index.md b/site/src/content/docs/index.md new file mode 100644 index 00000000..acc5cd2c --- /dev/null +++ b/site/src/content/docs/index.md @@ -0,0 +1,48 @@ +--- +title: "What is LemmaScript?" +description: "TypeScript with syntax for contracts — an agent writes the contract and the code together, and only correct code ships." +--- + + + +LemmaScript is **TypeScript with syntax for contracts** — the way TypeScript is +JavaScript with syntax for types. You (or your agent) write ordinary TypeScript and +add `//@ ` annotations stating what a function must do. The `lsc` toolchain +translates the code to a prover — Dafny or Lean 4 — and checks that the +implementation actually meets the spec. Contracts add **zero runtime cost** and work +on **existing codebases**, one function at a time. + +It's built agent-first: the agent writes the contract and the implementation +together and iterates until the check passes. You review the contract — a few +declarative lines — instead of the implementation. + +## What it looks like + +An agent splitting 10 three ways once floored each share and called it done: +`[3, 3, 3]` — that's 9, not 10; a cent vanished. With a contract, that +implementation can't survive: + +```typescript +//@ contract Splits total across weights so every unit is accounted for. +//@ requires total >= 0 +//@ requires weights.length >= 1 +//@ requires forall(k, 0 <= k && k < weights.length ==> weights[k] >= 0) +//@ requires sum(weights) >= 1 +//@ ensures sum(\result) === total // must sum to the whole +function allocate(total: number, weights: number[]): number[] { + // the floor-and-forget version fails this ensures; + // the fix hands the leftover back out — and passes +} +``` + +`lsc check` rejects the buggy version, the agent reads the failure and fixes the +code, and only the correct version surfaces. + +## Where to start + +- **[Installation](/installation/)** — Node, Dafny, the `lsc` toolchain, and the agent skills +- **[How the loop works](/how-the-loop-works/)** — the concepts in five minutes +- **[Add to an existing codebase](/getting-started/)** — start with one small function + +Prefer the full story? Read the [design rationale](/design/), or see what's been +built with it in the [case studies](/case-studies/). diff --git a/site/src/content/docs/installation.md b/site/src/content/docs/installation.md new file mode 100644 index 00000000..4d9f5d2f --- /dev/null +++ b/site/src/content/docs/installation.md @@ -0,0 +1,76 @@ +--- +title: "Installation" +description: "Install the lsc toolchain from npm and add the agent skills — or clone the source kit with everything bundled." +--- + + + +Two ways in. Use the **package** if you're using LemmaScript; take the **kit** if +you're changing it. + +## Option A — the package + +The standard setup: the `lsc` toolchain from npm, plus the skills that teach your +agent to drive it. + +### 1. Check the prerequisites + +- **Node.js ≥ 18** +- **[Dafny ≥ 4.x](https://dafny.org/latest/Installation)** — the prover that does the checking +- **git** + +```sh +node -v # ≥ 18 +dafny --version # ≥ 4.x +``` + +For the optional Lean backend you'll also need **Lean 4** (managed via `elan`/`lake`). + +### 2. Install the package + +One global install puts `lsc` — and companions like `lsc claimcheck` — on your PATH: + +```sh +npm install -g lemmascript +``` + +### 3. Add the skills + +Mount the [lemmascript-skills](https://github.com/midspiral/lemmascript-skills) repo +at your agent's skills directory — e.g. `.claude/skills` for Claude Code. Your agent +picks them up and drives the whole loop itself: contracts, checks, iteration. + +```sh +git clone https://github.com/midspiral/lemmascript-skills +``` + +### 4. Check something + +```sh +lsc check --backend=dafny path/to/file.ts +``` + +## Option B — from source: lemmascript-kit + +Working on the toolchain itself, or want the tools and skills pinned together? +[lemmascript-kit](https://github.com/midspiral/lemmascript-kit) bundles the toolchain +source and the skills as git submodules — one clone, one setup script, skills +already in place at `.claude/skills/`. + +```sh +git clone --recurse-submodules https://github.com/midspiral/lemmascript-kit.git +cd lemmascript-kit +./setup.sh +``` + +Run the same commands straight out of the source tree (the skills write the CLI as +`npx lsc`; in the kit, substitute this form or `npm link` the package): + +```sh +npx tsx LemmaScript/tools/src/lsc.ts check --backend=dafny path/to/file.ts +``` + +## Next + +- [CLI reference](/reference/cli/) — every `lsc` command diff --git a/site/src/content/docs/reference/cli.md b/site/src/content/docs/reference/cli.md new file mode 100644 index 00000000..12f6bb7d --- /dev/null +++ b/site/src/content/docs/reference/cli.md @@ -0,0 +1,130 @@ +--- +title: "CLI reference (lsc)" +description: "Every lsc command, flag, and file convention — gen, check, regen, extract, info, claimcheck, and batch mode." +--- + + + +The `lsc` command drives the whole toolchain. Install it globally +(`npm install -g lemmascript`) or run it from a source checkout with +`npx tsx tools/src/lsc.ts`. + +```sh +lsc [--backend=lean|dafny] [flags] +lsc [--backend=…] [--slow] # no file: batch over LemmaScript-files.txt +lsc claimcheck [] [flags…] # forwards to lemmascript-claimcheck +``` + +All flags use the `--flag=value` form. Space-separated flags (`--backend lean`) and +unknown flags are rejected with an error rather than silently ignored. Every command +exits `0` on success and `1` on any failure. + +## Commands + +| Command | What it does | +|---|---| +| `lsc gen ` | Generate backend code next to the source file | +| `lsc gen-check ` | `gen`, then verify the hand-edited file is additions-only vs. the generated one (Dafny) | +| `lsc check ` | `gen` + additions-only check + run the prover — the full loop | +| `lsc regen ` | Regenerate after a TS edit, three-way-merging to preserve proof additions (Dafny) | +| `lsc extract ` | Dump the Raw IR as JSON to stdout (backend-neutral) | +| `lsc info ` | Write `.ts.json`, a per-function spec summary (backend-neutral) | +| `lsc claimcheck []` | Check each function's plain-English `//@ contract` against its formal clauses | + +### `lsc gen` + +Generates the backend files next to your TypeScript source. + +- **Dafny** (`--backend=dafny`, the default): writes `.dfy.gen` (always + regeneratable — never edit) and, on first run, `.dfy` (the file you and your + proofs own; starts as a copy of `.dfy.gen`). +- **Lean** (`--backend=lean`): writes `.types.lean` (when the module declares + types) and `.def.lean`. + +### `lsc check` + +The whole loop for one file: generate, confirm the diff between `.dfy` and +`.dfy.gen` is **additions-only**, then run the prover (`dafny verify`, or +`lake build` for Lean). Passes only when every contract holds. + +```sh +lsc check --backend=dafny src/domain.ts +lsc check --backend=dafny --time-limit=120 src/domain.ts +lsc check --backend=dafny --extra-flags="--isolate-assertions" src/domain.ts +``` + +### `lsc regen` + +After editing the TypeScript, regenerate **without losing proof work**: the new +generated code is three-way-merged into `.dfy` (using `.dfy.base`), +preserving your helper lemmas, ghost predicates, and asserts, then re-verified. + +Never delete `.dfy` and `gen` fresh — you'd lose every proof addition. +`regen` is the safe path. Use `--no-verify` to run only the merge and +additions-only check, skipping the prover (CI uses this when a separate `check` +pass does the verifying). + +### `lsc extract` and `lsc info` + +Backend-neutral: they run regardless of any `//@ backend` directive. + +- `extract` prints the structured Raw IR as JSON — the supported way for external + tools to consume LemmaScript's frontend instead of re-parsing TypeScript. +- `info` writes `.ts.json`: each function's signature plus its `requires` / + `ensures` / `decreases` clauses. Tools like `lemmascript-seal` build on this. + +### `lsc claimcheck` + +Forwards to the bundled `lemmascript-claimcheck` CLI, which cross-examines the +plain-English `//@ contract` line against the formal clauses. With a file, it checks +that file (extra flags pass through verbatim); with no file, it runs once per entry +in `LemmaScript-files.txt`. + +## Batch mode + +Run `gen`, `gen-check`, or `check` with **no file argument** to batch over +`LemmaScript-files.txt` in the current directory — one entry per line: + +``` +src/domain.ts +src/allocate.ts 120 +src/scanner.ts 300 --isolate-assertions +``` + +Format: `filepath [timeout_in_seconds] [extra prover flags…]`. Batching is +fail-fast — the first failing entry stops the run. + +One safeguard: in a `check` batch (Dafny), entries whose timeout exceeds **60 +seconds** are downgraded to `gen-check` (generation + additions-only, no proving) so +routine runs stay fast. Pass `--slow` to verify every entry with its full timeout. + +## Flags + +| Flag | Applies to | Meaning | +|---|---|---| +| `--backend=dafny\|lean` | all except extract/info | Backend to target. Default: `dafny` | +| `--time-limit=` | check, regen | Prover time limit (positive integer) | +| `--extra-flags="…"` | check, regen | Extra flags passed to the prover verbatim | +| `--slow` | batch `check` | Verify long-timeout entries instead of downgrading them | +| `--no-verify` | regen | Merge + additions-only check only; skip the prover | + +## In-file directives the CLI honors + +| Directive | Effect | +|---|---| +| `//@ backend ` | The file belongs to one backend; commands for the other backend skip it (`extract`/`info` always run) | +| `//@ safe-slice` | File-level option consumed by the Dafny emitter | +| `//@ lean-module ` | Overrides the Lean module base name (Lean module names are global; this prevents collisions between identically-named files) | + +## Project resolution + +`lsc` resolves imports using the **nearest `tsconfig.json`** above the source file; +without one it falls back to strict ESNext defaults. From a source checkout, the +equivalent of `lsc` is `npx tsx /tools/src/lsc.ts` — no build step needed. + +## Next + +- [Installation](/installation/) — get `lsc` on your PATH +- [Supported TypeScript subset](/subset/) — what the toolchain can express +- [Full specification](/spec/) — precise semantics of the annotation language diff --git a/site/src/content/docs/tutorials/hello-lemmascript.md b/site/src/content/docs/tutorials/hello-lemmascript.md index 1d5b5bce..00bb4c99 100644 --- a/site/src/content/docs/tutorials/hello-lemmascript.md +++ b/site/src/content/docs/tutorials/hello-lemmascript.md @@ -1,5 +1,5 @@ --- -title: "Step 3: Hello LemmaScript" +title: "Hello, LemmaScript" description: "Write your first verified function and see what success and failure look like." --- diff --git a/site/src/content/docs/tutorials/quorum/00-introduction.md b/site/src/content/docs/tutorials/quorum/00-introduction.md index 57ac89b2..305a0746 100644 --- a/site/src/content/docs/tutorials/quorum/00-introduction.md +++ b/site/src/content/docs/tutorials/quorum/00-introduction.md @@ -21,7 +21,7 @@ Formal verification extends that idea to *behavior*. Instead of just "this funct ## What you'll use - **LemmaScript**: a toolchain that takes your TypeScript code, reads special comments you've added, and generates a formal model that a theorem prover can check. Your TypeScript runs unchanged; the verification is a parallel process. -- **Dafny**: the theorem prover that checks your proofs. You won't write Dafny directly (LemmaScript generates it and an agent completes proof), but you'll see its output when verification succeeds or fails. +- **Dafny**: the theorem prover that checks your proofs. You won't write Dafny directly (LemmaScript generates it and an agent completes the proofs), but you'll see its output when verification succeeds or fails. - **An AI agent** (like Claude Code or Codex): your partner for this build. You'll describe what you want; the agent will draft code and specifications. You review, modify, and direct. ## AI use diff --git a/site/src/content/docs/tutorials/quorum/01-setup.md b/site/src/content/docs/tutorials/quorum/01-setup.md index 8e346b6f..786141a3 100644 --- a/site/src/content/docs/tutorials/quorum/01-setup.md +++ b/site/src/content/docs/tutorials/quorum/01-setup.md @@ -24,35 +24,38 @@ Confirm: dafny --version ``` -## Set up your workspace +## Install LemmaScript -LemmaScript needs to be a sibling directory to your project. Create a parent folder that holds both: +One global install puts the `lsc` toolchain (and companions like `lsc claimcheck`) +on your PATH: ```bash -git clone --recursive https://github.com/midspiral/lemmascript-kit quorum-tutorial -cd quorum-tutorial +npm install -g lemmascript ``` -LemmaScript (https://github.com/midspiral/LemmaScript.git) should already be cloned inside it: -```bash -cd LemmaScript -npm install && npm run build -cd .. -``` +## Set up your workspace + +Create the project, then clone the agent skills into it — they teach your agent the +annotation grammar and the verification loop, and they carry the Quorum design +document you'll use in the next step: -Create your app directory next to it, as a sibling: ```bash mkdir quorum && cd quorum npm init -y npm install typescript --save-dev +git clone https://github.com/midspiral/lemmascript-skills ``` +`` is wherever your agent discovers skills — for Claude Code +that's `.claude/skills`; other agents have their own location. The tutorial uses +the placeholder throughout; substitute your path. + Your file structure: ``` -quorum-tutorial/ -├── .claude/skills/ ← the skills for AI (cloned) -├── LemmaScript/ ← the toolchain (cloned) -└── quorum/ ← your app (you are here) +quorum/ +├── / ← the skills for AI (cloned) +├── package.json +└── (src/ comes later) ``` ## Verify the toolchain @@ -68,7 +71,7 @@ EOF ``` ```bash -npx tsx ../LemmaScript/tools/src/lsc.ts gen --backend=dafny hello.ts +lsc gen --backend=dafny hello.ts dafny verify hello.dfy ``` @@ -84,8 +87,8 @@ rm hello.ts hello.dfy hello.dfy.gen ## What you've done -- Installed Dafny (the theorem prover) and LemmaScript (the toolchain) -- Set up a sibling directory layout: `LemmaScript/` next to `quorum/` +- Installed Dafny (the theorem prover) and the LemmaScript toolchain from npm +- Created the project with the agent skills mounted at your agent's skills directory - Verified the full pipeline works: annotated TypeScript → generated Dafny → proof passes ## Next step diff --git a/site/src/content/docs/tutorials/quorum/02-design.md b/site/src/content/docs/tutorials/quorum/02-design.md index 7e6bbb54..e153aac0 100644 --- a/site/src/content/docs/tutorials/quorum/02-design.md +++ b/site/src/content/docs/tutorials/quorum/02-design.md @@ -33,7 +33,7 @@ The document has a consistent structure: For this tutorial, we've written the DESIGN.md for you. It describes a when2meet-style scheduling app whose verified core guarantees: -**Note: When building on your own, you can use our design-doc skill, which is in `quorum-tutorial/.claude/skills/design-doc`** +**Note: When building on your own, you can use our design-doc skill, which is in `/lemmascript-design-doc`** 1. The heatmap counts are exact 2. The best-time recommendation flags the actual argmax slots @@ -44,7 +44,7 @@ For this tutorial, we've written the DESIGN.md for you. It describes a when2meet Copy it into your project root: ```bash -cp ../.claude/skills/design-doc/DESIGN_QUORUM.md ./DESIGN.md +cp /lemmascript-design-doc/DESIGN_QUORUM.md ./DESIGN.md ``` Read through it. The sections you'll interact with most in the next steps: @@ -55,7 +55,7 @@ Read through it. The sections you'll interact with most in the next steps: ## For your own app -When building your own verified app, use the `design-doc` skill provided to tell your agent: +When building your own verified app, use the `lemmascript-design-doc` skill provided to tell your agent: > I want to build [description of your app]. Write a DESIGN.md following the LemmaScript > design document format. @@ -64,7 +64,7 @@ The agent will draft the full document. Review it the same way: does the promise ## A note on design specs -This design doc is a starting point. While having a good understanding of your app domain is important when making initial decisions about what to verify and the shape of the core, iteration will be inevitible. +This design doc is a starting point. While having a good understanding of your app domain is important when making initial decisions about what to verify and the shape of the core, iteration will be inevitable. ## What you've done diff --git a/site/src/content/docs/tutorials/quorum/03-domain-core.md b/site/src/content/docs/tutorials/quorum/03-domain-core.md index 6f8e2df5..1ac57688 100644 --- a/site/src/content/docs/tutorials/quorum/03-domain-core.md +++ b/site/src/content/docs/tutorials/quorum/03-domain-core.md @@ -6,7 +6,7 @@ description: "Translate the design document into a verified domain model." ## What this step produces A single file: `src/domain.ts`. -[Sample.](https://github.com/midspiral/quorum-tutorial-lemmascript/blob/main/src/domain.dfy) +[Sample.](https://github.com/midspiral/quorum-tutorial-lemmascript/blob/main/src/domain.ts) This is the verified core. Everything else in the app (UI, network, storage) will import from this file and should never duplicate its logic. ## Tell your agent what to do diff --git a/site/src/content/docs/tutorials/quorum/04-verify.md b/site/src/content/docs/tutorials/quorum/04-verify.md index 2eca22b1..8397f684 100644 --- a/site/src/content/docs/tutorials/quorum/04-verify.md +++ b/site/src/content/docs/tutorials/quorum/04-verify.md @@ -15,14 +15,18 @@ Verification is iterative. You write annotations, generate Dafny, run the prover The command: ```bash -npx tsx ../LemmaScript/tools/src/lsc.ts check --backend=dafny src/domain.ts +lsc check --backend=dafny src/domain.ts ``` This does three things in sequence: -1. Generates `domain.dfy.gen` (the Dafny translation, never edit this) -2. Creates or merges `domain.dfy` (the working file where proof additions go) +1. Generates `domain.dfy.gen` (the Dafny translation, never edit this) and, on the + first run, creates `domain.dfy` as a copy of it (the working file where proof + additions go) +2. Checks that the diff between `domain.dfy` and `domain.dfy.gen` is additions-only 3. Runs `dafny verify domain.dfy` +(Merging after a TypeScript change is `regen`'s job, covered below.) + ## What success looks like ``` @@ -143,7 +147,7 @@ The agent adds proofs to `domain.dfy`. When you later change the TypeScript and **After any TypeScript change, always use regen (not gen):** ```bash -npx tsx ../LemmaScript/tools/src/lsc.ts regen --backend=dafny src/domain.ts +lsc regen --backend=dafny src/domain.ts ``` ## Common gotchas diff --git a/site/src/content/docs/tutorials/quorum/05-proof-review.md b/site/src/content/docs/tutorials/quorum/05-proof-review.md index d9a9ae34..0ffefcf1 100644 --- a/site/src/content/docs/tutorials/quorum/05-proof-review.md +++ b/site/src/content/docs/tutorials/quorum/05-proof-review.md @@ -13,7 +13,7 @@ Proofs passing doesn't mean you've proven everything the design promised. Dafny ## Open a fresh agent -This works best in a **new agent with no context** from the build process. A clean agent reads the files from scratch and isn't biased by the iteration it just went through. We recommend using this `proof-review` skill to guide the agent. +This works best in a **new agent with no context** from the build process. A clean agent reads the files from scratch and isn't biased by the iteration it just went through. We recommend using the `lemmascript-proof-review` skill (in your skills directory) to guide the agent. If you use the skill, simply call it from the agent; no further instructions needed. diff --git a/site/src/content/docs/tutorials/quorum/07-iteration.md b/site/src/content/docs/tutorials/quorum/07-iteration.md index 16830bb2..2cc39997 100644 --- a/site/src/content/docs/tutorials/quorum/07-iteration.md +++ b/site/src/content/docs/tutorials/quorum/07-iteration.md @@ -51,10 +51,11 @@ export function participantCount(e: Event): number { ### Verify ```bash -npx tsx ../LemmaScript/tools/src/lsc.ts regen --backend=dafny src/domain.ts -dafny verify src/domain.dfy +lsc regen --backend=dafny src/domain.ts ``` +(`regen` re-verifies after merging, so no separate `dafny verify` is needed.) + This one should auto-discharge: the body directly returns the ensures expression. No proof work needed in the `.dfy` file. ### Use it in the UI @@ -106,8 +107,7 @@ export function participationRate(e: Event, s: number): number { ### Verify — expect a fight ```bash -npx tsx ../LemmaScript/tools/src/lsc.ts regen --backend=dafny src/domain.ts -dafny verify src/domain.dfy +lsc regen --backend=dafny src/domain.ts ``` This is where it gets real. The proof involves multiplication (`* 100`) and