ch:information-flow: ch:information-flow
Problem and invariant. Every assignment joins its expression label with the current program-counter label. The independent two-run oracle compares exactly the variables visible at the selected observer.
Two representations. A source-set analysis gives richer diagnostics. The companion uses their two-point label join, the exact abstraction required by the displayed rules.
First complete version. Implement flow, join, expression labels, and command checking. Thread the pc through branches and loops, then add fuel-bounded evaluation and pairwise result comparison.
Observable result. Six passes cover leak rejection, password-audit acceptance, a secure rejected program, public-to-secret flow, mutant acceptance, and its two-run counterexample.
A failing version. The included badCheck omits the guard label. It accepts
Acceptance test. Run the four appendix E commands and require the exact transcript and empty audit. Then add the exercise’s three-point lattice cases.
Mathematical boundary. Fuel exhaustion is treated as non-observation. The finite test does not prove TINI for every terminating derivation or termination-sensitive security.