Pin that every aborting model effect also refuses (improvise-we1a)

Host::mutating_frame rejects on refused || aborted, and deleting the
aborted arm left the workspace green. The wire table cannot see an
abort-without-refuse because that arm is what rejects it, so the new
table applies each failing ModelCommand's effects to a bare App and
asserts it refused, pinning which cases abort so it is not vacuous.
The arm is kept as defence: AbortChain shows an abort need not be an
error, so making abort-without-refuse unconstructible is declined.

Also keeps rtud's three key-path table rows (load, import-json of an
absent JSON, a formula that does not parse) as added coverage; rtud's
prose fix lands separately.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
Edward Langley
2026-09-23 08:06:45 -07:00
parent 345a35895e
commit eb061391fe
4 changed files with 210 additions and 0 deletions
+24
View File
@@ -609,6 +609,30 @@ the client was told nothing at all.
`AddItem` case the same way and found none, so `AddItem` does not stop either.
An abort is added where a later effect depends on the failed one, never for
symmetry.
- **The `|| last_batch_aborted()` arm is kept, and the invariant it guards is
pinned (improvise-we1a).** Every model effect that aborts today also refuses,
so deleting the arm left the workspace green: nothing tested it. There were
two ways to close that. One was to make an abort without a refusal
impossible to write. The other, taken here, was to test the invariant with
the arm left in place. `every_failing_model_effect_that_aborts_also_refuses`
applies each failing `ModelCommand`'s own effects to an `App`, bypassing
`Host`, and asserts it refused. It also pins which cases abort, so it cannot
pass on a table that aborts nothing. The wire table cannot hold this
invariant, because the arm itself rejects a frame that aborted without
refusing. With AddCategory's arm reverted to status-only, the wire table
stays green. The option not taken is right for today's rules and wrong for
the future:
- `AbortChain` aborts without refusing, correctly. It is `ViewOnly`, and it
stops a chain whose premise no longer holds, which is not an error. A
type-level rule of "every abort refuses" would first have to exempt it.
- Making it refuse would change which `:` lines the headless CLI reports as
failures.
- Keeping the raw `abort_effects` setter away from `Model` effects alone would
be a new visibility split, and today no effect needs it.
So the arm stays, as defence for a future `Model` effect that aborts on
something other than an error. The test is what says the arm is currently
redundant, and it will fail when that stops being true.
In a client's frame, any refusal becomes `Rejected(MutationRefused)`. The frame
is undone whole, and the client is told, which is the channel the narrated
+41
View File
@@ -5697,3 +5697,44 @@ host's `Normal`, and nothing else different. `install_workbook` needs no
change of its own, because both of its callers (`LoadModel`,
`AcceptWizardModel`) run inside `apply_effects`, which settles after the batch.
## `ui/host.rs` — the abort arm of `Host::mutating_frame` (improvise-we1a)
### every_failing_model_effect_that_aborts_also_refuses
What the gap was: `Host::mutating_frame` rejects a frame when
`last_batch_refused() || last_batch_aborted()`. Every model effect that aborted
also refused, so deleting the `|| last_batch_aborted()` arm left all tests
passing. The wire table (`every_failing_model_command_refuses_its_whole_frame`)
cannot hold the invariant, because that arm rejects a frame that aborted
without refusing. The test applies each failing `ModelCommand`'s own effects,
from `model_effects`, straight to an `App`, and asserts that the batch refused.
Each case also carries whether it aborts. That catches a table in which nothing
aborts, and a site that quietly stops aborting.
Faults injected:
- `AddCategory`'s failure arm set `status_msg` and aborted, but did not refuse.
- This test failed, and so did the key-path table.
- The wire table passed, which is the gap.
- With the arm also deleted, `a_refused_mutation_rolls_back_its_predecessor_and_the_abort_flag`
failed as well. So the arm is what makes the wire table look correct under
this fault.
- `refuse_and_stop` wrote the status and aborted without refusing. This test
failed, as did the key-path table,
`a_failed_load_or_import_does_not_run_the_quit_after_it` and
`a_formula_that_does_not_parse_keeps_the_user_in_the_editor_with_their_text`.
The wire table passed.
### every_refusal_site_refuses_its_failure_and_only_its_failure — three cases (improvise-rtud)
This entry covers the rows `load of an absent file`, `import-json of an absent
JSON` and `a formula that does not parse`. Each has a succeeding twin
(`load doc.improv` from `MemoryFs`, `import-json good.json`, `Total = 1`).
Each row was checked by a rival at its own site: the `refuse_and_stop` call in
`AddFormula`'s parse arm, in `LoadModel`, or in the JSON read arm of
`ImportJsonHeadless`, replaced by a status write plus the abort. Under each
rival, the table fails at that row. The matching row of
`every_failing_model_effect_that_aborts_also_refuses` fails too. A rival in
`refuse_and_stop` itself is no use here, because the table stops at its first
failing row, which is the older `import-json of an absent CSV`. The rtud prose correction is landing separately, so these
rows are coverage only.
+39
View File
@@ -3244,6 +3244,21 @@ mod tests {
app
}
/// Storage holding one loadable document, `doc.improv`, and nothing else.
fn with_a_document_to_load() -> App {
let storage = crate::storage::MemoryFs::new();
let text = crate::persistence::format_md(&Workbook::new("Doc"));
crate::storage::Storage::write(
&storage,
std::path::Path::new("doc.improv"),
text.as_bytes(),
)
.expect("fixture writes");
let mut app = two_col_model();
app.storage = Box::new(storage);
app
}
fn with_a_second_view(mut app: App) -> App {
app.model_state.workbook.create_view("Second");
app
@@ -3437,6 +3452,30 @@ mod tests {
run_line(app, "search-navigate forward")
},
),
(
"load of an absent file",
with_a_document_to_load,
|app| run_line(app, "load absent.improv"),
"Load error",
with_a_document_to_load,
|app| run_line(app, "load doc.improv"),
),
(
"import-json of an absent JSON",
|| with_import_fixtures(two_col_model()),
|app| run_line(app, "import-json absent.json"),
"Cannot read 'absent.json'",
|| with_import_fixtures(two_col_model()),
|app| run_line(app, "import-json good.json"),
),
(
"a formula that does not parse",
two_col_model,
|app| commit_in(app, AppMode::formula_edit(), "formula", "Total = ("),
"Formula error",
two_col_model,
|app| commit_in(app, AppMode::formula_edit(), "formula", "Total = 1"),
),
(
"a : line that does not parse",
two_col_model,
+106
View File
@@ -1985,6 +1985,112 @@ mod tests {
}
}
/// improvise-we1a: `mutating_frame`'s `|| last_batch_aborted()` arm is redundant
/// only while this holds. Evidence: `context/test-evidence/command.md`.
#[test]
fn every_failing_model_effect_that_aborts_also_refuses() {
let fresh = || {
let mut wb = workbook();
wb.create_view("Scratch");
(0..12).for_each(|n| drop(wb.add_category(format!("Filler{n}"))));
let mut app = App::new(wb, None);
app.storage = Box::new(super::import_fixture_storage());
app.rebuild_layout();
app
};
let cases: Vec<(&str, ModelCommand, bool)> = vec![
(
"AddCategory past the limit",
ModelCommand::AddCategory("Extra".into()),
true,
),
(
"AddFormula that does not parse",
ModelCommand::AddFormula {
raw: "Total = (".into(),
target_category: "_Measure".into(),
},
true,
),
(
"LoadModel of an absent file",
ModelCommand::LoadModel(PathBuf::from("absent.improv")),
true,
),
(
"import of an absent JSON",
import("absent.json", None),
true,
),
("import of an absent CSV", import("absent.csv", None), true),
(
"import of a CSV that is not text",
import("bad.csv", None),
true,
),
(
"import of JSON that does not parse",
import("bad.json", None),
true,
),
(
"import at a path with no array",
import("nested.json", Some("nope")),
true,
),
(
"import that builds no model",
import("measures.json", None),
true,
),
(
"AddItem into an absent category",
ModelCommand::AddItem {
category: "Ghost".into(),
item: "East".into(),
},
false,
),
(
"AddItemInGroup into an absent category",
ModelCommand::AddItemInGroup {
category: "Ghost".into(),
item: "East".into(),
group: "Coastal".into(),
},
false,
),
(
"AddFormula into an absent category",
ModelCommand::AddFormula {
raw: "Total = 1".into(),
target_category: "Ghost".into(),
},
false,
),
(
"DeleteView of an absent view",
ModelCommand::DeleteView("Ghost".into()),
false,
),
];
for (what, cmd, aborts) in cases {
let mut app = fresh();
let effects = crate::ui::reduce::model_effects(&app, &cmd);
app.apply_effects(effects);
assert_eq!(
app.last_batch_aborted(),
aborts,
"{what}: which failures abort is part of what this table pins"
);
assert!(
app.last_batch_refused(),
"{what}: failed without refusing, so a frame carrying it is rejected \
only by mutating_frame's `|| last_batch_aborted()` arm"
);
}
}
/// improvise-9fpl: one case per refusal #181 converted that no other test
/// witnesses. Evidence: `context/test-evidence/command.md`.
#[test]