Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/).

### Added

- Pace and frame the cast of `rune proof run` for a reader: a rule per capability, a boxed title and kind line per scene, typed commands, a tick or cross per step, `--pause` between scenes, a tally.
- Read `# text` lines in a console fence as comments: dim in the cast, recorded in the transcript with the command lines, compared by `--check`.
- Add proof frontmatter (`type: proof`, `change`, `head`, `recorded`, `transcript`, `scenes`) that `rune graph export` reads.
- Emit `rune:Proof` with a proves edge per proven scene, only while `proof.txt` matches the recorded transcript.
- Add proof README validation to `rune spec validate`: a malformed field or an instruction scene without a model fails the run and names the field.
Expand Down Expand Up @@ -209,6 +211,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/).

### Fixed

- Number a console fence error by the line of the README file, not of the body under the frontmatter.
- Fix `rune run --clean` for codex: the clean `config.toml` keeps every `[model_providers.*]` table with its `auth` and names the one custom provider as the route.
- Fix `rune run grok@grok --clean-harness-state` exiting 127 through the `harness-run` shim: the clean run names the real `~/.grok/bin` in `HARNESS_REAL_BIN_DIR` before it moves `HOME`.
- Fix the identity tests to expect the versioned display names the synced `author-identity.py` derives (`Claude Fable 5.2`, not `Claude`).
Expand Down
51 changes: 51 additions & 0 deletions docs/changes/proof-scene-layout/adr.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
---
title: "A proof cast is paced and framed for a reader"
description: "rune proof run writes the cast on a presentation timeline with one frame vocabulary per scene, so a person can read a GIF and a page shows the same scene a transcript records"
type: adr
category: architecture
tags:
- cli
- proof
- cast
status: proposed
created: 2026-09-27
updated: 2026-09-27
author: "@N4M3Z"
project: cli
related:
- "DECK-0015 Behavior Proof per Change"
- "DECK-0019 A Proof Plays as a Cast Where a Person Reads It"
responsible: ["@N4M3Z"]
accountable: ["@N4M3Z"]
consulted: ["claude-fable-5-1", "gpt-6-astra"]
informed: []
upstream:
- "https://docs.asciinema.org/manual/asciicast/v2/"
change: proof-scene-layout
---

# A proof cast is paced and framed for a reader

## Context and Problem Statement

A proof has two readers. The transcript binds the claim and is read by `rune proof run --check` and by the graph. The cast is read by a person, on a page or as a GIF, and the person decides whether to sign. `rune proof run` writes the cast at real offsets, so a proof of fast commands is one frame of output with no typed command, and the deck's bash driver holds the layout the owner picked. Which timeline and which frame vocabulary should the cast carry?

## Considered Options

1. Real time. The cast shows what the clock saw. Honest about duration, unreadable for fast commands, and different from the driver's layout.
2. Presentation time with the driver's layout. The cast writes fixed pauses and types each command, one frame vocabulary for a proof and for a session recording, and the transcript alone binds the claim.
3. Post-process the real-time cast in the deck. The layout lives in a second tool, every proof needs two steps, and a page can show a cast the run never wrote.

## Decision Outcome

Option 2. The cast MUST be paced for a reader: a fixed pause after each scene (`--pause`, default 3 s), a shorter one after a header or a comment, and each command typed word by word behind a prompt. Each scene MUST open with a boxed `N/T · title` and a kind line naming the requirement, each capability with a rule naming it and its scene count, and the cast MUST close with a tally. Each step MUST end with one tick that names the exit status and the match, or a red cross with the reason. A fence comment `# text` MUST show dim and italic before its command and MUST be part of the transcript. The transcript stays the record. The cast's offsets are a reading aid and never evidence of duration.

Option 1 keeps the reader out. Option 3 splits the layout from the run and lets a page play a cast that differs from the transcript.

### Consequences

- [+] One frame vocabulary for a proof, a session recording, and the page's scene list, in the layout the owner already chose.
- [+] A GIF of a fast proof is readable without the page.
- [-] The cast no longer tells how long a command took. A proof that wants duration on record puts it in the output.
- [-] Every recorded cast re-records to gain the layout, in the deck and in the cli.
- [-] Comments in a fence join the transcript, so adding one to a recorded proof changes its digest and needs a re-run.
31 changes: 31 additions & 0 deletions docs/changes/proof-scene-layout/proposal.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
---
adr: docs/changes/proof-scene-layout/adr.md
status: proposed
decisions: ["A proof cast is paced and framed for a reader"]
---

# Proof scene layout

## Why

`rune proof run` writes `proof.cast` from the captured output at real offsets. Twenty-three scenes of a fast command sit inside the first 0.2 seconds. No typed command appears, and the only marker between scenes is a blue rule with a `# Scenario:` line that carries the whole scenario key. A person who opens the GIF sees one frame of output and cannot tell which command produced it. The deck's fallback driver `prove.sh` has the layout the owner picked on 2026-09-25: a capability rule, a boxed `N/T · title`, a kind line, dim comments, a typed command behind a prompt, the output, one green tick per expectation, and a closing tally. That layout exists only in bash, so a proof recorded by rune and one recorded by the driver look different.

## What Changes

- The cast `rune proof run` writes is paced for a reader, not by the clock: a fixed pause after each scene (`--pause`, default 3 s), a shorter one after a header or a comment. Each command is typed word by word behind a prompt.
- Each scene opens with a boxed `N/T · title` and a kind line that names the requirement. Each capability opens with a rule that carries its name and scene count. The cast closes with a tally.
- A fence line `# text` before a command is a comment. The cast shows it dim and italic, and the transcript records it with the command lines.
- Each step ends with one tick that names the exit status and that the output matched; a failed step ends with a red cross and the first line of the reason.
- The transcript `proof.txt` and its digest change only by the comment lines a README adds.

## Capabilities

### New Capabilities

- proof-scene-layout

## Impact

- `src/cli/proof/fence.rs` (comment lines), `src/cli/proof/runner.rs` (per-step verdicts), `src/cli/proof/mod.rs` (the cast writer and pacing), `src/cli/mod.rs` (`--pause`).
- Every recorded `proof.cast` re-records to gain the layout. The transcripts hold unless a README adds comments.
- The deck's AcceptanceTesting skill drops `prove.sh` as the layout's home once this merges. The page tooling renders both proof and session casts in one frame vocabulary.
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
# proof-scene-layout

## Purpose

How the cast `rune proof run` writes reads for a person: the presentation timeline, the frame vocabulary per scene, and the fence comments that explain a step.

## ADDED Requirements

### Requirement: The Cast Is Paced For A Reader

The run MUST write `proof.cast` on a presentation timeline rather than the clock: a rule per capability with its name and scene count, a boxed `N/T · title` and a kind line naming the requirement per scene, each command typed word by word behind a prompt with its input lines, its output, then one green tick naming the exit status and the match, or a red cross with the reason. A fixed pause (`--pause`, default 3 s) separates the scenes and a tally closes the cast.

#### Scenario: Scenes are paced for a reader

- **WHEN** a proof of three scenes whose commands finish within a millisecond runs with the default pause
- **THEN** the cast's last event sits past nine seconds, each scene's box and tick are separate events, and no two scenes share a second

#### Scenario: Owner shortens the pause

- **WHEN** the run is started with `--pause 0.5`
- **THEN** consecutive scene boxes in the cast sit about half a second apart plus the scene's own typing and output time

#### Scenario: Failed step shows its reason in the cast

- **WHEN** a step's output disagrees with the fence
- **THEN** the cast shows the command, its output, and a red cross line that starts with `unproven:` and states the difference, and the tally counts the scene as unproven

### Requirement: A Fence Comment Explains The Step

A line `# text` inside a console fence, before a command, MUST be a comment: the runner shows it dim and italic in the cast before the command it precedes, records it in the transcript with that command's lines, and `--check` compares it like a command line. A comment after a command's input lines belongs to the next command. A comment with no command after it is a fence error that names the line.

#### Scenario: Comment before a command

- **WHEN** a fence holds `# the guard refuses rm -rf` above `$ rune hook run --harness claude --native-event PreToolUse`
- **THEN** the cast shows the comment dim before the typed command and `proof.txt` holds the comment line above the command line

#### Scenario: Comment with no command

- **WHEN** a fence ends with a comment line and no command after it
- **THEN** the run fails before any scene runs and names the line of the dangling comment
18 changes: 18 additions & 0 deletions docs/changes/proof-scene-layout/tasks.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
# Tasks

## 1. Fence comments

- [ ] 1.1 `src/cli/proof/fence.rs`: `# text` lines before a command parse as that step's comments, join `command_lines`, a dangling comment is a fence error naming its line
- [ ] 1.2 Tests: a comment before a command, a comment after input lines belongs to the next command, a dangling comment

## 2. Cast layout and pacing

- [ ] 2.1 `src/cli/proof/cast.rs`: the presentation timeline (`Cast` with pauses), the capability rule, the scene box and kind line, the dim comment, the typed command and input lines, the output, the tick and the cross, the tally
- [ ] 2.2 `src/cli/proof/runner.rs`: per-step outcomes (command lines, output, exit, match or reason) for the cast writer
- [ ] 2.3 `src/cli/proof/mod.rs` and `src/cli/mod.rs`: `--pause <seconds>` on `rune proof run`, the run assembles the cast through the writer
- [ ] 2.4 Tests: three fast scenes sit past nine seconds with the default pause, `--pause 0.5` spaces the boxes by about half a second, a failed step's cross and the tally, the transcript unchanged by the layout

## 3. Proof and records

- [ ] 3.1 Re-record `docs/proofs/harness-hook-dispatch` and this change's own proof with the layout
- [ ] 3.2 CHANGELOG entries, the deck's AcceptanceTesting skill points at `rune proof run` for the layout
112 changes: 112 additions & 0 deletions docs/proofs/proof-scene-layout/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,112 @@
---
type: proof
change: proof-scene-layout
head: 275680d7a3efd4752c679f42d529c078895fec9f
recorded: 2026-10-16
transcript: f5a7cb262873035586a08e60c10c2a11a43a675dcf8e985b61b0cb51d3aa9207
scenes:
- scenario: proof-scene-layout#the-cast-is-paced-for-a-reader/scenes-are-paced-for-a-reader
kind: check
- scenario: proof-scene-layout#the-cast-is-paced-for-a-reader/owner-shortens-the-pause
kind: check
- scenario: proof-scene-layout#the-cast-is-paced-for-a-reader/failed-step-shows-its-reason-in-the-cast
kind: check
- scenario: proof-scene-layout#a-fence-comment-explains-the-step/comment-before-a-command
kind: check
- scenario: proof-scene-layout#a-fence-comment-explains-the-step/comment-with-no-command
kind: check
---

# Proof: proof-scene-layout

One scene per scenario, in closure order. The scenes copy a proof fixture under `tests/fixtures/proof/`, run `rune proof run` on the copy, and read the cast it wrote back with a short Python script fed through the fence.

## proof-scene-layout#the-cast-is-paced-for-a-reader/scenes-are-paced-for-a-reader

```console
# three scenes whose commands finish within a millisecond, default pause
$ sh -c 'cp -Rf "$RUNE_PROOF_ROOT/tests/fixtures/proof/paced" repo && rune proof run sample-change-one --source repo >/dev/null'
$ python3 -
< import json
< events = [json.loads(l) for l in open("repo/docs/proofs/sample-change-one/proof.cast").readlines()[1:]]
< boxes = [t for t, _, d in events if "\u250c" in d]
< ticks = [t for t, _, d in events if "\u2713" in d]
< print("last event past nine seconds:", events[-1][0] > 9)
< print("boxes:", len(boxes), "ticks:", len(ticks))
< print("seconds shared by two scenes:", len(boxes) - len({int(t) for t in boxes}))
last event past nine seconds: True
boxes: 3 ticks: 3
seconds shared by two scenes: 0
```

## proof-scene-layout#the-cast-is-paced-for-a-reader/owner-shortens-the-pause

```console
# the same proof at --pause 0.5 and at the default; the box gap shrinks by 2.5 s
$ sh -c 'cp -Rf "$RUNE_PROOF_ROOT/tests/fixtures/proof/paced" slow && cp -Rf "$RUNE_PROOF_ROOT/tests/fixtures/proof/paced" fast && rune proof run sample-change-one --source slow >/dev/null && rune proof run sample-change-one --pause 0.5 --source fast >/dev/null'
$ python3 -
< import json
< def gap(path):
< events = [json.loads(l) for l in open(path).readlines()[1:]]
< boxes = [t for t, _, d in events if "\u250c" in d]
< return boxes[1] - boxes[0]
< slow = gap("slow/docs/proofs/sample-change-one/proof.cast")
< fast = gap("fast/docs/proofs/sample-change-one/proof.cast")
< print("gap difference:", round(slow - fast, 2))
< print("fast gap under three seconds:", fast < 3)
gap difference: 2.5
fast gap under three seconds: True
```

## proof-scene-layout#the-cast-is-paced-for-a-reader/failed-step-shows-its-reason-in-the-cast

```console
# the first scene expects rune 0.5.0 and the run is newer
$ sh -c 'cp -Rf "$RUNE_PROOF_ROOT/tests/fixtures/proof/mismatch" repo && rune proof run sample-change-one --source repo'
? 1
sample-capability-one#thing-holds/version-prints ... unproven: output of `rune --version` differs:
- rune 0.5.0 ([..])
+ rune [..]
sample-capability-one#thing-holds/missing-tag-fails ... ok (check)
2 scenes, 1 proven, 1 unproven; transcript [..]
$ python3 -
< import json, re
< text = "".join(json.loads(l)[2] for l in open("repo/docs/proofs/sample-change-one/proof.cast").readlines()[1:])
< plain = re.sub(r"\x1b\[[0-9;]*m", "", text).replace("\r", "")
< start = plain.index("rune --version")
< print(plain[start:start + 40].splitlines()[0])
< print([l for l in plain.splitlines() if l.startswith("\u2717")][0])
< print(plain.splitlines()[-1])
rune --version
✗ unproven: output of `rune --version` differs:
2 scenes · 1 proven · 1 unproven
```

## proof-scene-layout#a-fence-comment-explains-the-step/comment-before-a-command

```console
# the third scene of the fixture carries a comment above its command
$ sh -c 'cp -Rf "$RUNE_PROOF_ROOT/tests/fixtures/proof/paced" repo && rune proof run sample-change-one --source repo >/dev/null'
$ grep -n -B1 -A1 '^# the shell' repo/docs/proofs/sample-change-one/proof.txt
[..]-kind: check
[..]:# the shell prints what it is given
[..]-$ printf 'one\n'
$ python3 -
< import json, re
< text = "".join(json.loads(l)[2] for l in open("repo/docs/proofs/sample-change-one/proof.cast").readlines()[1:])
< plain = re.sub(r"\x1b\[[0-9;]*m", "", text).replace("\r", "")
< lines = plain.splitlines()
< at = lines.index("# the shell prints what it is given")
< print("comment:", lines[at])
< print("then:", lines[at + 1])
comment: # the shell prints what it is given
then: ❯ printf 'one\n'
```

## proof-scene-layout#a-fence-comment-explains-the-step/comment-with-no-command

```console
$ sh -c 'cp -Rf "$RUNE_PROOF_ROOT/tests/fixtures/proof/dangling-comment" repo && rune proof run sample-change-one --source repo'
? 2
fatal: [..]README.md: line 20: a comment `# text` comes before the command it explains
```
Loading
Loading