Learn · All the Ways It Can Break

growing

Run Finds a World; Check Finds a Refutation

SAT means different things when the command asks for an example and when it challenges an assertion.

formal-methods, alloy, sat, assertions, counterexample, learn

You will write predicates and assertions, execute run and check with Alloy 6.2.0, read SAT/UNSAT by command kind, and retain a usefulness witness beside a security check.

Grade every command

The executable commands are:

alloy code/all-the-ways-it-can-break/document-sharing/Sharing.als#commands Sharing.als The test declares the expected polarity for every command: SAT, UNSAT, SAT.

Run the model from the Analyzer or with the official distribution's command-line exec mode. Inspect the instance for BugBlocksStranger: the tuple Stranger -> Document is the refutation. Then inspect GuestCanRead: the same SAT label now denotes a desired witness.

Interpretation — attach SAT to the question that produced it.

Assertions do not constrain worlds

A fact always constrains every command. A predicate constrains a command only when invoked. An assertion states a claim to challenge; it does not make itself true. Moving a desired property into a fact before checking it makes the check vacuous because every counterexample was excluded by assumption.

Negative and positive controls

The buggy assertion is a negative control: a known bad policy must be refuted. The guest run is a positive witness: useful sharing remains satisfiable. The fixed check sits between them. Together they resist a disconnected assertion, an overconstrained model, and an allow-nobody “repair.”

Lessons

run searches for satisfying examples; check searches for assertion counterexamples.
SAT/UNSAT polarity depends on command kind.
Facts constrain; predicates describe; assertions are challenged.
Every command needs an expected verdict in automated evidence.
A security check needs a usefulness witness to resist overconstraint.

Practice

Retrieval. Interpret all four combinations of run/check and SAT/UNSAT.
Discrimination. Why is moving FixedBlocksStranger into a fact before checking suspicious?
Transfer. Add a run showing the owner can read and state its expected verdict.

Worked answers

Run SAT: example; run UNSAT: no example in scope; check SAT: counterexample; check UNSAT: no counterexample in scope.
The fact removes refuting worlds by assumption, making the assertion circular.
run OwnerCanRead { FixedPolicy Owner -> Document in Access.grants } for 5, expected SAT.

References

AlloyTools. Alloy tutorial. — facts, predicates, assertions, run, and check
AlloyTools. Alloy 6.2.0 release. — the checked tool version

← Join Replaces the Pointer Chase A Small Scope Still Needs a Witness →

run asks whether at least one world satisfies a predicate. SAT supplies the requested example; UNSAT says none exists in scope. check asks whether a counterexample to an assertion exists. SAT supplies a refutation; UNSAT says no counterexample exists in scope. The solver vocabulary is the same, but the human conclusion reverses. The document-sharing specimen grades all three commands. The buggy assertion is SAT because a stranger reads. The fixed assertion is UNSAT because no counterexample exists in scope. A separate run is SAT because a guest can still read, preventing “security” from meaning “deny everyone.”