Proof: ellipsis dot-run normalization is locally idempotent and protection-stable

[leynos]

Proof target: ellipsis dot-run normalization

Relevant code: src/ellipsis.rs (replace_dot_runs), ADR 0005.

For a maximal unprotected dot run of length n, the implementation emits "…" * (n / 3) followed by "." * (n % 3). Since 0 <= n % 3 < 3, no replaceable triple remains in that run.

Goals

• Local correctness. replace_dot_runs(s) maps each maximal run of n dots to ⌊n/3⌋ ellipses and n mod 3 dots, and preserves every non-dot character in order.
• Local idempotence. replace_dot_runs(replace_dot_runs(s)) == replace_dot_runs(s).
• Protection stability (the important part). A region protected on the first run (URL, path, code span, code block, per ADR 0005) is still protected on the second run. Proving the arithmetic does not establish this; it requires that the emitted ellipsis characters cannot create or destroy a protection boundary.

Implementation recipe

1. Verify replace_dot_runs over Seq<char> with a spec fn normalize_runs, proving by induction on the run structure. This is a self-contained beginner-level Verus target and a good first kernel for the harness.
2. Specify the protection predicate spec fn protected(s, i) -> bool for the region scanner in src/ellipsis/; treat the URL/path regexes as external contracts in the ledger.
3. Prove lemma_ellipsis_char_is_neutral: inserting … at an unprotected position does not change protected at any other position. This is the lemma that makes the whole-feature idempotence follow.
4. Ledger: local correctness and local idempotence; protection stability is a cross-pass result and depends on the fence kernel for code blocks.

Non-vacuity tests

• Witness proofs: "a....b" yields "a….b"; "......" yields "……"; ".." unchanged.
• Mutation: emit n % 3 + 1 trailing dots and confirm the idempotence lemma fails on the "......" witness (which would gain a triple).
• Executable: the existing tests/data ellipsis fixtures plus the fence reproduction from the unmatched-block issue as a negative case (literal... inside a fence must be untouched).

Related issues

• Harness: Verification harness: adopt rust-prover-tools for Verus install and run, add claim ledger #479. Fence kernel for code-block protection: Proof: fence transition kernel and LEM-FENCE-NORMALIZATION-PRESERVES-REGIONS #486. Tracking: Composition theorem: per-pass normal forms with establishment, stability, and preservation obligations (tracking) #494.

[leynos]

@CodeRabbit plan

[coderabbitai]

Coding Plan

Summary

Extract a pure, character-based dot-run kernel from replace_dot_runs so Verus can verify the function the formatter actually calls, and include it in verus/lib.rs with #[path].

Prove local correctness and local idempotence over Seq<char> by induction, using 0 <= n % 3 < 3 as the fixed-point fact, with witness proofs and a documented mutation check for non-vacuity.

Specify the protected predicate with external_body contracts for URL and path recognition, and prove lemma_ellipsis_char_is_neutral for inline regions, deferring code-block cross-pass stability to the fence kernel (#486).

Register the landed claims in the ledger, add an unmatched-fence negative test, and author the phase-based execplan.

Design Choices

Design Choice 1: How the proof must reach the executable code that the formatter calls

Options Considered:

1. Keep the regex conversion in production and verify a separate re-implemented kernel. This risks drift and breaks the "no standalone reimplementation" rule unless backed by a refinement proof.
2. Replace the regex conversion inside a small pure kernel exec fn that scans characters, then make replace_dot_runs delegate to that kernel. Include the kernel in verus/lib.rs with #[path] and verify it directly.

Chosen Option: 2

Rationale: Option 2 makes the verified function the one the formatter calls. It avoids drift. It removes the regex from the proof boundary, so no external_body contract is needed for the core arithmetic. replace_dot_runs uses the regex crate, which Verus cannot verify directly. ADR 0011 requires the theorem to apply to the executable function.

Design Choice 2: How much of protection stability can land in this ticket

Options Considered:

1. Land the complete cross-pass protection-stability theorem now.
2. Land the local kernel proof, the protected predicate, and the neutrality lemma for inline regions now. Treat URL/path recognition and code-block protection as external contracts. Defer the full cross-pass theorem to issue #486.

Chosen Option: 2

Rationale: The ticket states that protection stability is a cross-pass result that depends on the fence kernel. Land the local proofs and the neutrality lemma now and record the deferred dependency. Full cross-pass protection stability depends on the fence kernel for code-block protection (issue #486), which has not landed.

💡 User Tips

Regenerate the plan with different choices with @coderabbitai <feedback>.

Implementation Steps

Phase 1: Extract a pure, verifiable dot-run kernel

Refactor the production code so the ellipsis arithmetic lives in a small pure function that Verus can include and verify. Keep observable behaviour identical.

Task 1: Extract the dot-run kernel exec fn

Move the run-conversion arithmetic out of the regex closure and into a pure, character-based function.

• Add a new pure exec fn in src/ellipsis.rs (or a new src/ellipsis/kernel.rs module included by ellipsis.rs). Name it precisely, for example normalize_dot_runs, because the ledger check requires an exact fn name in src/.
• Make the kernel scan characters left to right. For each maximal run of n dots, emit n / 3 … characters and n % 3 leftover . characters. Copy every non-dot character in order.
• Do not use regex inside the kernel. Verus cannot reason about the regex engine.
• Change replace_dot_runs to delegate to the kernel. Keep the &str in / String out surface unchanged. Retain the DOT_RE.is_match fast path only if it stays outside the kernel and does not change output; otherwise remove it.
• Keep the kernel free of String::len-as-width assumptions. The kernel works on characters, not display columns.

Task 2: Add witness and mutation unit tests

Add function-level tests next to replaces_long_sequences in src/ellipsis.rs.

• Add witness cases: "a....b" yields "a….b", "......" yields "……", and ".." stays unchanged.
• Add a Rust-level idempotence assertion for the kernel: normalize_dot_runs(normalize_dot_runs(s)) equals normalize_dot_runs(s) for the witness inputs and for the existing long-sequence cases.
• Keep these tests as a fast regression guard that mirrors the Verus claims.

🤖 Prompt for AI agents

Implement Phase 1: extract a pure, verifiable dot-run kernel from the
regex-based ellipsis transform, keeping observable behaviour identical.

- In `src/ellipsis.rs` (or a new `src/ellipsis/kernel.rs` module included by
`ellipsis.rs`), add a new pure exec fn named precisely, for example
`normalize_dot_runs`. Use an exact name because the ledger check requires an
exact `fn` name in `src/`.
- Make the kernel scan characters left to right. For each maximal run of `n`
dots, emit `n / 3` `…` characters followed by `n % 3` leftover `.` characters.
Copy every non-dot character in order.
- Do not use the `regex` crate inside the kernel, because Verus cannot reason
about the regex engine.
- Change `replace_dot_runs` to delegate to the kernel. Keep the `&str` in /
`String` out surface unchanged. Retain the `DOT_RE.is_match` fast path only if
it stays outside the kernel and does not change output; otherwise remove it.
- Keep the kernel free of `String::len`-as-width assumptions: work on
characters, not display columns.
- Add function-level tests next to `replaces_long_sequences` in
`src/ellipsis.rs`: witness cases `"a....b"` → `"a….b"`, `"......"` → `"……"`, and
`".."` stays unchanged.
- Add a Rust-level idempotence assertion for the kernel:
`normalize_dot_runs(normalize_dot_runs(s))` equals `normalize_dot_runs(s)` for
the witness inputs and for the existing long-sequence cases. Keep these tests as
a fast regression guard that mirrors the Verus claims.

Phase 2: Prove local correctness and local idempotence in Verus

Add the first real kernel to the harness. Specify the transform over Seq<char> and prove correctness and idempotence by induction.

Task 1: Specify the transform and include the kernel

Add the spec model and wire the kernel into the proof entry point.

• Add spec fn normalize_runs over Seq<char> in the kernel module. Model the same run rule: each maximal run of n dots becomes n / 3 … characters and n % 3 dots, with every non-dot character preserved in order.
• Use recursive structure over Seq<char> with a decreases clause on sequence length, per Verus induction guidance.
• Model positions as Unicode scalar indices in the spec. Do not mix scalar indices with byte offsets.
• Include the kernel module in verus/lib.rs with a #[path] attribute inside the verus! { ... } block. Do not reimplement the kernel in verus/lib.rs.

Task 2: Prove correctness and idempotence

Add the proof lemmas that establish the two local claims.

• Prove that the kernel exec fn refines normalize_runs (local correctness): the executable output equals the spec output for all inputs.
• Prove local idempotence: normalize_runs(normalize_runs(s)) =~= normalize_runs(s). Use extensional sequence equality (=~=).
• Drive the induction on run structure. In each step, unfold one run, apply the induction hypothesis on the tail, and use Seq concatenation lemmas.
• State the key fact explicitly: because 0 <= n % 3 < 3, the output run contains fewer than three consecutive dots, so a second pass finds no replaceable triple.

Task 3: Add witness proofs and a mutation non-vacuity self-test

Add proof-level evidence that the claims are not vacuous.

• Add proof fn witnesses in verus/lib.rs (or the kernel module) that assert normalize_runs on concrete inputs: "a....b" gives "a….b", "......" gives "……", and ".." is unchanged.
• Document the mutation check in the execplan (Phase 4): change the kernel to emit n % 3 + 1 trailing dots and confirm the idempotence lemma then fails on the "......" witness, which would gain a triple. Do not commit the mutated kernel; record it as a manual non-vacuity experiment.
• Confirm make verus accepts the new kernel and make verus-selftest still rejects verus/smoke.rs.

🤖 Prompt for AI agents

Implement Phase 2: add the first real kernel to the Verus harness by specifying
the dot-run transform over `Seq<char>` and proving correctness and idempotence
by induction.

- Add `spec fn normalize_runs` over `Seq<char>` in the kernel module. Model the
same run rule as the exec fn: each maximal run of `n` dots becomes `n / 3` `…`
characters and `n % 3` dots, with every non-dot character preserved in order.
- Use recursive structure over `Seq<char>` with a `decreases` clause on sequence
length, per Verus induction guidance.
- Model positions as Unicode scalar indices in the spec. Do not mix scalar
indices with byte offsets.
- Include the kernel module in `verus/lib.rs` with a `#[path]` attribute inside
the `verus! { ... }` block. Do not reimplement the kernel in `verus/lib.rs`.
- Prove that the kernel exec fn refines `normalize_runs` (local correctness):
the executable output equals the spec output for all inputs.
- Prove local idempotence: `normalize_runs(normalize_runs(s)) =~=
normalize_runs(s)`, using extensional sequence equality (`=~=`).
- Drive the induction on run structure: in each step, unfold one run, apply the
induction hypothesis on the tail, and use `Seq` concatenation lemmas.
- State explicitly that because `0 <= n % 3 < 3`, the output run contains fewer
than three consecutive dots, so a second pass finds no replaceable triple.
- Add `proof fn` witnesses in `verus/lib.rs` (or the kernel module) asserting
`normalize_runs` on concrete inputs: `"a....b"` gives `"a….b"`, `"......"` gives
`"……"`, and `".."` is unchanged.
- Document the mutation check for Phase 4's execplan: change the kernel to emit
`n % 3 + 1` trailing dots, confirm the idempotence lemma then fails on the
`"......"` witness (it would gain a triple), and record it as a manual
non-vacuity experiment without committing the mutated kernel.
- Confirm `make verus` accepts the new kernel and `make verus-selftest` still
rejects `verus/smoke.rs`.

Phase 3: Specify the protection predicate and the neutrality lemma

Specify what "protected" means and prove that emitting … at an unprotected position does not move any protection boundary. Scope the code-block part as a deferred cross-pass dependency.

Task 1: Specify the protection predicate with external contracts

Model the region scanner of src/ellipsis/protected.rs as a spec.

• Add spec fn protected(s: Seq<char>, i: int) -> bool that states whether scalar position i lies inside a protected region (URL, path, code span, code block, per ADR 0005).
• Model the literal_spans output invariants already encoded by the proptest literal_spans_are_valid_and_disjoint: sorted, disjoint, and boundary-aligned regions.
• Wrap URL and path recognition (the current regex and prefix heuristics) as #[verifier::external_body] contracts. State only the recognition contract. Do not assert idempotence or protection stability inside these contracts.
• Keep byte offsets, scalar indices, and display columns as distinct types when relating literal_spans byte ranges to the scalar-indexed protected predicate.

Task 2: Prove lemma_ellipsis_char_is_neutral

Add the lemma that makes whole-feature idempotence follow.

• State lemma_ellipsis_char_is_neutral: inserting a … character at an unprotected position does not change protected at any other position.
• Prove that a … character is not part of any URL, path, link, or autolink token boundary, so it cannot create or destroy a protection boundary for inline regions.
• Scope code-block protection as an external contract for now. Note that fenced and indented code regions are excluded before literal_spans runs, through the shared FenceTracker.

Task 3: Record the deferred cross-pass dependency

Document the boundary between what lands now and what waits for the fence kernel.

• State clearly that the full cross-pass protection-stability theorem depends on the fence kernel for code blocks (issue #486).
• Land the inline-region neutrality result now. Record the code-block part as a tracked follow-up.

🤖 Prompt for AI agents

Implement Phase 3: specify the protection predicate and prove that emitting `…`
at an unprotected position does not move any protection boundary, while
deferring the code-block part as a cross-pass dependency.

- Model the region scanner of `src/ellipsis/protected.rs` as a spec. Add `spec
fn protected(s: Seq<char>, i: int) -> bool` stating whether scalar position `i`
lies inside a protected region (URL, path, code span, code block, per ADR 0005).
- Model the `literal_spans` output invariants already encoded by the proptest
`literal_spans_are_valid_and_disjoint`: sorted, disjoint, and boundary-aligned
regions.
- Wrap URL and path recognition (the current regex and prefix heuristics) as
`#[verifier::external_body]` contracts. State only the recognition contract. Do
not assert idempotence or protection stability inside these contracts.
- Keep byte offsets, scalar indices, and display columns as distinct types when
relating `literal_spans` byte ranges to the scalar-indexed `protected`
predicate.
- State `lemma_ellipsis_char_is_neutral`: inserting a `…` character at an
unprotected position does not change `protected` at any other position.
- Prove that a `…` character is not part of any URL, path, link, or autolink
token boundary, so it cannot create or destroy a protection boundary for inline
regions.
- Scope code-block protection as an external contract for now, noting that
fenced and indented code regions are excluded before `literal_spans` runs,
through the shared `FenceTracker`.
- Record clearly that the full cross-pass protection-stability theorem depends
on the fence kernel for code blocks (issue `#486`). Land the inline-region
neutrality result now and record the code-block part as a tracked follow-up.

Phase 4: Ledger, fixtures, and execution plan document

Register the claims, add executable non-vacuity coverage, and author the execplan.

Task 1: Update the verification ledger

Add the landed claims to docs/verification.md.

• Add a row for local correctness. Set "Executable function" to the exact kernel name, for example normalize_dot_runs. Set "Result class" to local correctness.
• Add a row for local idempotence against the same executable function. Set "Result class" to byte-level idempotence.
• List the URL and path recognition external contracts in the "Unverified external contracts" column. Do not restate the property under proof.
• Confirm make lint (which runs scripts/check-verification-ledger.sh) accepts the exact symbol names.

Task 2: Add the fence unmatched-block negative fixture

Add executable coverage that a literal dot run inside a fence stays untouched.

• Extend the existing coverage in tests/cli/ellipsis.rs (an active target). Do not rely on tests/wrap/fence_behaviour.rs, which is not wired into an active integration target.
• Add a negative case that combines an unclosed fence (the flush_unmatched_block pattern from src/fences.rs) with --ellipsis. Assert that a literal... inside the unmatched fence stays unchanged.
• Reuse the existing ellipsis fixtures under tests/data as the positive corpus.
• State the non-vacuity of the negative case: assert the input actually contains a triple-dot run inside the fence, so the "unchanged" assertion cannot pass vacuously.

Task 3: Author the execplan document

Add a phase-based execution plan under docs/execplans/.

• Follow the existing execplan structure: reminder banner, Status: line, Issue: link, ## Purpose / big picture, ## Constraints, ## Verification plan (### Axioms, ### Obligations, ### Rigour and residual gaps), ## Milestones and plateaus (### EP-M0, ### EP-M1, …), and ## Interfaces and dependencies with per-file line budgets.
• Attach a non-vacuity statement to each verification obligation, in the style of check-option.md and git-option.md.
• Record the mutation experiment from Task 2.3 in the verification plan.
• Reference the related issues: harness #479, fence kernel #486, tracking #494.

🤖 Prompt for AI agents

Implement Phase 4: register the landed claims in the verification ledger, add
executable non-vacuity coverage, and author the execplan document.

- Add rows to `docs/verification.md`: one row for local correctness with
"Executable function" set to the exact kernel name (for example
`normalize_dot_runs`) and "Result class" set to local correctness; one row for
local idempotence against the same executable function with "Result class" set
to byte-level idempotence.
- List the URL and path recognition external contracts in the "Unverified
external contracts" column. Do not restate the property under proof.
- Confirm `make lint` (which runs `scripts/check-verification-ledger.sh`)
accepts the exact symbol names.
- Extend the existing coverage in `tests/cli/ellipsis.rs` (an active target). Do
not rely on `tests/wrap/fence_behaviour.rs`, which is not wired into an active
integration target.
- Add a negative case combining an unclosed fence (the `flush_unmatched_block`
pattern from `src/fences.rs`) with `--ellipsis`. Assert that a `literal...`
inside the unmatched fence stays unchanged.
- Reuse the existing ellipsis fixtures under `tests/data` as the positive
corpus.
- Assert the non-vacuity of the negative case: confirm the input actually
contains a triple-dot run inside the fence, so the "unchanged" assertion cannot
pass vacuously.
- Add a phase-based execution plan document under `docs/execplans/`, following
the existing execplan structure: reminder banner, `Status:` line, `Issue:` link,
`## Purpose / big picture`, `## Constraints`, `## Verification plan` (`###
Axioms`, `### Obligations`, `### Rigour and residual gaps`), `## Milestones and
plateaus` (`### EP-M0`, `### EP-M1`, …), and `## Interfaces and dependencies`
with per-file line budgets.
- Attach a non-vacuity statement to each verification obligation, in the style
of `check-option.md` and `git-option.md`.
- Record the mutation experiment from Task 2.3 in the verification plan.
- Reference the related issues: harness `#479`, fence kernel `#486`, tracking `#494`.

Research

The --ellipsis transform lives in src/ellipsis.rs. replace_dot_runs converts each maximal run of three or more dots with DOT_RE.replace_all, emitting len / 3 … characters and len % 3 leftover dots. Protection of URLs, paths, links, and autolinks lives in src/ellipsis/protected.rs (literal_spans), which returns sorted, disjoint, char-boundary-aligned byte ranges. Fenced and indented code regions are excluded earlier in ellipsis.rs through the shared FenceTracker and tokenize_markdown.

The Verus harness is a scaffold. verus/lib.rs is the sole production proof entry point; kernels must be included there with #[path] or connected by a refinement proof. verus/smoke.rs is a deliberately failing proof used as a non-vacuity self-test. docs/verification.md holds the claim ledger table, and scripts/check-verification-ledger.sh requires each "Executable function" name to be an exact fn declaration in src/. ADR 0011 requires distinct types for byte offsets, Unicode scalar indices, and display columns, and requires #[verifier::external_body] contracts to never restate the property under proof. verus/ is not a Cargo member; the pinned Verus toolchain supplies vstd.

---

🚀 Next Steps

🤖 All AI agent prompts combined

Task: 1

Implement Phase 1: extract a pure, verifiable dot-run kernel from the
regex-based ellipsis transform, keeping observable behaviour identical.

- In `src/ellipsis.rs` (or a new `src/ellipsis/kernel.rs` module included by
`ellipsis.rs`), add a new pure exec fn named precisely, for example
`normalize_dot_runs`. Use an exact name because the ledger check requires an
exact `fn` name in `src/`.
- Make the kernel scan characters left to right. For each maximal run of `n`
dots, emit `n / 3` `…` characters followed by `n % 3` leftover `.` characters.
Copy every non-dot character in order.
- Do not use the `regex` crate inside the kernel, because Verus cannot reason
about the regex engine.
- Change `replace_dot_runs` to delegate to the kernel. Keep the `&str` in /
`String` out surface unchanged. Retain the `DOT_RE.is_match` fast path only if
it stays outside the kernel and does not change output; otherwise remove it.
- Keep the kernel free of `String::len`-as-width assumptions: work on
characters, not display columns.
- Add function-level tests next to `replaces_long_sequences` in
`src/ellipsis.rs`: witness cases `"a....b"` → `"a….b"`, `"......"` → `"……"`, and
`".."` stays unchanged.
- Add a Rust-level idempotence assertion for the kernel:
`normalize_dot_runs(normalize_dot_runs(s))` equals `normalize_dot_runs(s)` for
the witness inputs and for the existing long-sequence cases. Keep these tests as
a fast regression guard that mirrors the Verus claims.
===============================================================================

Task: 2

Implement Phase 2: add the first real kernel to the Verus harness by specifying
the dot-run transform over `Seq<char>` and proving correctness and idempotence
by induction.

- Add `spec fn normalize_runs` over `Seq<char>` in the kernel module. Model the
same run rule as the exec fn: each maximal run of `n` dots becomes `n / 3` `…`
characters and `n % 3` dots, with every non-dot character preserved in order.
- Use recursive structure over `Seq<char>` with a `decreases` clause on sequence
length, per Verus induction guidance.
- Model positions as Unicode scalar indices in the spec. Do not mix scalar
indices with byte offsets.
- Include the kernel module in `verus/lib.rs` with a `#[path]` attribute inside
the `verus! { ... }` block. Do not reimplement the kernel in `verus/lib.rs`.
- Prove that the kernel exec fn refines `normalize_runs` (local correctness):
the executable output equals the spec output for all inputs.
- Prove local idempotence: `normalize_runs(normalize_runs(s)) =~=
normalize_runs(s)`, using extensional sequence equality (`=~=`).
- Drive the induction on run structure: in each step, unfold one run, apply the
induction hypothesis on the tail, and use `Seq` concatenation lemmas.
- State explicitly that because `0 <= n % 3 < 3`, the output run contains fewer
than three consecutive dots, so a second pass finds no replaceable triple.
- Add `proof fn` witnesses in `verus/lib.rs` (or the kernel module) asserting
`normalize_runs` on concrete inputs: `"a....b"` gives `"a….b"`, `"......"` gives
`"……"`, and `".."` is unchanged.
- Document the mutation check for Phase 4's execplan: change the kernel to emit
`n % 3 + 1` trailing dots, confirm the idempotence lemma then fails on the
`"......"` witness (it would gain a triple), and record it as a manual
non-vacuity experiment without committing the mutated kernel.
- Confirm `make verus` accepts the new kernel and `make verus-selftest` still
rejects `verus/smoke.rs`.
===============================================================================

Task: 3

Implement Phase 3: specify the protection predicate and prove that emitting `…`
at an unprotected position does not move any protection boundary, while
deferring the code-block part as a cross-pass dependency.

- Model the region scanner of `src/ellipsis/protected.rs` as a spec. Add `spec
fn protected(s: Seq<char>, i: int) -> bool` stating whether scalar position `i`
lies inside a protected region (URL, path, code span, code block, per ADR 0005).
- Model the `literal_spans` output invariants already encoded by the proptest
`literal_spans_are_valid_and_disjoint`: sorted, disjoint, and boundary-aligned
regions.
- Wrap URL and path recognition (the current regex and prefix heuristics) as
`#[verifier::external_body]` contracts. State only the recognition contract. Do
not assert idempotence or protection stability inside these contracts.
- Keep byte offsets, scalar indices, and display columns as distinct types when
relating `literal_spans` byte ranges to the scalar-indexed `protected`
predicate.
- State `lemma_ellipsis_char_is_neutral`: inserting a `…` character at an
unprotected position does not change `protected` at any other position.
- Prove that a `…` character is not part of any URL, path, link, or autolink
token boundary, so it cannot create or destroy a protection boundary for inline
regions.
- Scope code-block protection as an external contract for now, noting that
fenced and indented code regions are excluded before `literal_spans` runs,
through the shared `FenceTracker`.
- Record clearly that the full cross-pass protection-stability theorem depends
on the fence kernel for code blocks (issue `#486`). Land the inline-region
neutrality result now and record the code-block part as a tracked follow-up.
===============================================================================

Task: 4

Implement Phase 4: register the landed claims in the verification ledger, add
executable non-vacuity coverage, and author the execplan document.

- Add rows to `docs/verification.md`: one row for local correctness with
"Executable function" set to the exact kernel name (for example
`normalize_dot_runs`) and "Result class" set to local correctness; one row for
local idempotence against the same executable function with "Result class" set
to byte-level idempotence.
- List the URL and path recognition external contracts in the "Unverified
external contracts" column. Do not restate the property under proof.
- Confirm `make lint` (which runs `scripts/check-verification-ledger.sh`)
accepts the exact symbol names.
- Extend the existing coverage in `tests/cli/ellipsis.rs` (an active target). Do
not rely on `tests/wrap/fence_behaviour.rs`, which is not wired into an active
integration target.
- Add a negative case combining an unclosed fence (the `flush_unmatched_block`
pattern from `src/fences.rs`) with `--ellipsis`. Assert that a `literal...`
inside the unmatched fence stays unchanged.
- Reuse the existing ellipsis fixtures under `tests/data` as the positive
corpus.
- Assert the non-vacuity of the negative case: confirm the input actually
contains a triple-dot run inside the fence, so the "unchanged" assertion cannot
pass vacuously.
- Add a phase-based execution plan document under `docs/execplans/`, following
the existing execplan structure: reminder banner, `Status:` line, `Issue:` link,
`## Purpose / big picture`, `## Constraints`, `## Verification plan` (`###
Axioms`, `### Obligations`, `### Rigour and residual gaps`), `## Milestones and
plateaus` (`### EP-M0`, `### EP-M1`, …), and `## Interfaces and dependencies`
with per-file line budgets.
- Attach a non-vacuity statement to each verification obligation, in the style
of `check-option.md` and `git-option.md`.
- Record the mutation experiment from Task 2.3 in the verification plan.
- Reference the related issues: harness `#479`, fence kernel `#486`, tracking `#494`.

💡 Iterate on the plan with: `@coderabbitai` <feedback>

Example Feedback
- `@coderabbitai` You can skip phase 3. Add a simple unit test case for phase 2.
- `@coderabbitai` For design choice 1 go ahead with option 3 and replan.

---