# Formal verification / Leanstral pump surface

Maintained verification surface for EtherCalc pure integer models. **Shipping
TypeScript remains the oracle.** LemmaScript provides a reduced integer model:

| Track | Role |
| ----- | ---- |
| Dafny (`lsc check --backend=dafny`) | CI-checked VCs on the facade |
| Lean (`lsc gen --backend=lean`) | Generated models for Leanstral prompting |
| Bun tests | Only authority for production behavior |

Full `lake build` is **not** gated (needs sibling Loom/Velvet/LemmaScript
checkouts). CI only asserts Lean generation + non-empty + committed-fresh
artifacts. Context regeneration is **not** in CI (needs sibling SocialCalc).

## Layout

| Path | Role |
| ---- | ---- |
| `xlsx-a1.ts` | LemmaScript facade with `//@ requires` + correspondence limits |
| `xlsx-a1.{dfy,dfy.gen}` | Generated by `lsc` — must stay byte-identical (no hand proofs) |
| `xlsx-a1.{types,def}.lean` | Generated by `lsc gen --backend=lean` — do not hand-edit |
| `assert-fresh.mjs` | Asserts `.dfy == .dfy.gen` / Lean tree clean after gen |
| `build-context.mjs` | Deterministic context pack from shipping sources |
| `context.md` | Generated pack (`vp run verify:context`) |
| `prompt.md` | Open-ended Leanstral prompt template |
| `build-request.mjs` | Concatenates prompt + context + Lean → `request.md` |
| `request.md` | Generated Leanstral request (`vp run verify:request`) |
| `README.md` | This file (authoritative workflow) |

Root `LemmaScript-files.txt` lists facade paths for batch `lsc` mode.

## Commands (Vite+)

```bash
cd ~/w/ethercalc
vp install

# Dafny: generate + check VCs + assert .dfy == .dfy.gen
# Requires `dafny` on PATH (CI pins 4.9.0).
vp run verify:dafny

# After editing xlsx-a1.ts, rewrite both Dafny artifacts:
vp run verify:dafny:regen
# then: vp run verify:dafny   # should stay green

# Lean: generate models + non-empty smoke + committed-fresh check
vp run verify:lean

# Both
vp run verify:both

# Deterministic Leanstral context + request (sibling SocialCalc required)
vp run verify:context
vp run verify:request

# Pump (after context + lean gen + request)
omp --print --no-tools --no-session --mode text \
  --model mistral/labs-leanstral-1-5-1 @lemma/request.md
```

`verify:context` twice on unchanged sources must produce identical `context.md`
bytes. Same for `verify:request` after a frozen Lean gen.

### Sibling SocialCalc prerequisite (`verify:context` only)

`lemma/build-context.mjs` reads upstream bounds from:

- `../socialcalc/lemma/a1.ts`
- `../socialcalc/lemma/a1.dfy`

Clone [audreyt/socialcalc](https://github.com/audreyt/socialcalc) as a sibling
of this repo (`../socialcalc`). EtherCalc-only clones can still run
`verify:dafny` / `verify:lean` and use the **tracked** `lemma/context.md` +
`lemma/request.md` without regenerating. CI never runs `verify:context`.

## Generated-artifact freshness

This facade has **no hand proofs**. Policy:

1. After every facade edit: `vp run verify:dafny:regen` then commit both
   `xlsx-a1.dfy` and `xlsx-a1.dfy.gen` (must be identical).
2. `verify:dafny` runs `lsc check` then `assert-fresh.mjs dafny` (`cmp`-style
   equality of `.dfy` and `.dfy.gen`).
3. `verify:lean` regenerates Lean files then fails if git shows a diff
   (stale committed Lean).
4. CI re-runs check/gen and `git diff --exit-code` on the generated paths.

Do not hand-edit `.dfy`, `.dfy.gen`, or `*.lean`.

## What is / is not proved

**Proved (Dafny VCs on the facade):** integer-step contracts on
`isValidCol`, `encodeStep`, `encodeDigit`, `accumCol`, `toZeroBased`,
`roundTripCode`, `isWithinSocialCalc` under their `//@ requires`.

**Not proved:** string codecs (`encodeColumn`/`parseCoord` letter building),
SocialCalc `coordToCr`, HTTP routing, DO storage, clipboard range assembly.
Those are Bun-tested against shipping public APIs.

**IEEE-754 correspondence limit:** TypeScript `number` is reduced to
mathematical `Int` in Dafny/Lean. `NaN`, `±Infinity`, and non-integer
fractions are outside the model and must be Bun-tested (e.g. merge end
columns in `enforceSocialCalcColumnLimit`).

**Upstream SocialCalc** ([audreyt/socialcalc](https://github.com/audreyt/socialcalc)
`lemma/`) holds the 1-based A1 algebra (33 VCs). EtherCalc's facade is
0-based SheetJS-shaped; do not co-prove without an explicit 0↔1 shim.

## Promotion rules

1. Shipping TypeScript is the oracle. Model output is a hypothesis.
2. Every finding must be execution-checked against public APIs before promotion.
3. Promote only findings that become a new observable Bun assertion (or a
   **passing** defense of a plausible model-authored bug).
4. A passing regression that refutes a wrong model premise is still a valid
   promotion — it locks the adapter boundary the model challenged.

### Historical example (Attempt 2)

Leanstral claimed `colLetters(lastcol - 1)` underflows under the false premise
that `sheet.attribs.lastcol` is SheetJS 0-based. After `replayWorkbook`,
`lastcol` is SocialCalc **1-based** (A=1 … ZZ=702), so `lastcol - 1` is the
correct 0↔1 adapter. Promoted passing tests in
`packages/worker/test/xlsx-import.node.test.ts`:

- A1:ZZ1 clipboard → `copiedfrom\cA1\cZZ1` (not `ZY1`)
- A1-only clipboard → `copiedfrom\cA1\cA1` (not empty-column `A1:1`)

Immutable raw capture: [`spikes/leanstral-xlsx-coords/leanstral-raw.md`](../spikes/leanstral-xlsx-coords/leanstral-raw.md).
Immutable Attempt 2 request: [`spikes/leanstral-xlsx-coords/attempt-2-request.md`](../spikes/leanstral-xlsx-coords/attempt-2-request.md).

## Provenance

The first pump lived under `spikes/leanstral-xlsx-coords/`. That directory is
**immutable history** (Attempt 2 request + raw stdout). The maintained workflow
is this directory. Do not re-pump historical requests; regenerate from current
shipping sources via `verify:context` / `verify:request`.