Invariant, or check

Read these two statements about the Portal's first web rung. First: the web layer calls only the Portal facade. Second: for an unknown user id, the page renders the empty state. Both are true. But the first is universal — it claims something of every request the slice will ever serve. The second is one example — it claims something of one scenario.

That difference is the whole distinction. An invariant is universally quantified: for all values, at all times. It names a rule the increment must never break, and it is written once, in the spec's Invariants section. An acceptance check is existentially scoped: for this one case. It is written as a Given/When/Then on a story, and it proves one example. A spec carries both because they cover different things — the rule, and the example of the rule.

The two claims also live in two places. An invariant is written in the Invariants section of the spec (f6.1.md) — named once, with an id, exercised by checks. A check is written as a Given/When/Then on a story in f6.1.stories.md — one scenario, with its own acceptance criteria. Select a statement to see which artifact and section is its home.

This is not a filing detail. The home tells you the claim's scope: a statement in the Invariants section is a rule over all values; a Given/When/Then on a story is one named case. Reading the home is a fast way to tell an invariant from a check without parsing the sentence.

On the Portal — the learning platform this course builds — the first web rung F6.1 · Bootstrap the Phoenix PortalThe first web rung: stand the F5 engine up as a Phoenix app, with one facade-backed route and a liveness route. The F6.1 draft named a /courses/:user_id page; F6.5 renamed it to the protected /my/courses — a learner's own enrollments.View the spec ladder → carries both kinds of claim. The Invariants section of f6.1.md names the master invariant, F6.1-INV1: a rule the whole web layer obeys for every request. The stories file f6.1.stories.md carries F6.1-US5, whose first Given/When/Then is one scenario: an authenticated learner with no enrollments sees the empty state at the protected /my/courses. Read side by side, the universal rule and the one example are easy to tell apart.

The fragment below is the two claims, verbatim — the invariant line from the spec and the scenario from the story. No code, only spec text: the rule, and one example of the slice behaving.

# f6.1.md — Invariants (a rule over ALL values, named once).
#   F6.1-INV1 (master): the web layer calls only the Portal facade and renders
#   only the closed %Portal.Error{} set. No controller, LiveView, plug, or
#   template names Portal.Engine, a repo, or GenServer.call.   → INVARIANT (∀ request)

# f6.1.stories.md — F6.1-US5 acceptance (ONE scenario).
#   Given an authenticated learner with no enrollments,
#   When  GET /my/courses (the learner's own courses, protected),
#   Then  the page renders the empty state — a clean 200.   → CHECK (∃ this case)

An invariant holds for every value, always — it is universally quantified, named once in the Invariants section, and exercised by checks. An acceptance check holds for one scenario — it is one Given/When/Then on a story. They are different kinds of claim, written in different homes, and a rung is done only when every invariant holds and every check passes. With the two told apart, the next dive reads the one invariant the Portal's web chapter rests on.

Primary sources for the invariant-against-check distinction, and where it connects in the course.