Try to break this

The claim

When a program withdraws a piece of evidence, Caveat erases nothing, flags every current value that was computed from it, and lets the program reopen exactly the decisions whose recorded grounds include it, while each past decision keeps the basis it actually had.

1. R1 Nothing recorded changes. Every observation, every decision's frozen basis and grounds, and every journal entry stay as they were. The withdrawal is added as its own record. (Withdrawal 0.1, step 3)
2. R2 Everything computed from it is flagged. Every current value whose lineage or grounds hold the withdrawn evidence carries the caveat withdrawn, including values read through a decision that rested on it. A value that never touched it does not. (step 2)
3. R3 "Rests on" means grounds, exactly. rests_on_withdrawn(D) is true when, and only when, the current revision of D has withdrawn evidence in its frozen grounds. (Predicates)
4. R4 Nothing reopens by itself. A withdrawal changes no decision's status. Only a rule or trigger the author wrote reopens one, and the journal records it.
5. R5 A refused event withdraws nothing. A withdrawal is part of its event's transaction.

What is outside the claim

• Evidence only a guard read. A when condition is control, not grounds, so withdrawing evidence that only opened a gate does not make rests_on_withdrawn true. Values computed under that guard still carry withdrawn through their lineage, and has_caveat(STATE, …) answers from grounds. The guard example below shows both. If you think this rule is wrong, a report that shows the harm is welcome.
• Whether the evidence was true, or whether the reason for withdrawing it was good. Caveat records both and judges neither (Limits).
• A program whose own rules choose not to reopen. Caveat gives the predicate; the author decides what it means.
• Saves edited by hand (saves are not authenticated), events refused by a resource cap, and undoing a withdrawal, which the language does not offer.

Run it

Start from an example or write your own program and events, one JSON object per line. Everything runs here, in your browser, on the WebAssembly runtime built from …. Nothing is sent anywhere.

Apartment example Guard-only example

Run and check

Loading the runtime…

How the checker works

After every event it reads the runtime's own snapshot and tests each rule: R1 compares every earlier record with the new snapshot, R2 compares each value's lineage with the withdrawal records, R3 recomputes "grounds hold withdrawn evidence" and compares it with the runtime's answer, R4 looks for an authored reopening behind every decision that reopened, and R5 checks that a refused event changed no withdrawal or decision. To ask the runtime for R3, it adds one display line per decision to your program; those lines change no state, evidence or decision. It checks the cases you run; it is not a proof. The code is break-check.js.

Reporting

The report button opens a new GitHub issue with your program, events and the failed rules filled in. You see it on GitHub before anything is submitted. Every report gets a reply saying whether it is a bug, a disagreement with a rule, or outside the claim, and why. A confirmed bug gets a regression test named after it and a patch release, and its reporter is credited in the release record unless they ask not to be. A disagreement with a rule is a question about the language itself, decided in the open (compatibility). You can also file one by hand with the break report template.