Lesson 23 of 23 · 3:35
A small end-to-end access-policy example
Build a bounded CM application with explicit inputs, outputs and exhaustive verification.
Keyboard: focus the player, then Space or K to play/pause and arrow keys to seek. Tab moves through the controls. Selectable captions replace the video's caption strip with the same timed text below.
In this lesson
- 0:00 · Can we check every case of an access policy?
- 0:24 · Choose the output contract
- 0:47 · Build the expression with the public API
- 1:04 · Compile and materialize the small truth layout
- 1:26 · Trace an allowed administrator case
- 1:47 · Change one fact: suspension
- 2:05 · Validate the policy exhaustively
- 2:26 · Your turn: does ownership override suspension?
- 2:50 · Answer: suspension still denies access
- 3:09 · Retain what makes the result reproducible
Complete transcript
This transcript includes the answers to prediction prompts.
Show transcript
Can we check every case of an access policy? · 0:00
Can we check every case of an access policy? Our document-access rule requires authentication, either ownership or administrator status, and no suspension. We will formalize the rule, compile it, and test all sixteen input combinations. You will learn to trace an allow or deny result back to the stated policy and identify the limits of this bounded example.
Choose the output contract · 0:24
Our query returns one bit: allow or deny for one specified combination of the four facts. For teaching and exhaustive checking, we will also materialize all sixteen answers. The rule does not verify identity or decide whether someone really is an administrator; those facts must come from a trusted surrounding system.
Build the expression with the public API · 0:47
Map the four facts to Var zero through Var three. Build owner OR administrator, AND that with authenticated, then AND the result with NOT suspended. The grouping follows the plain-language policy. Parentheses make the intended structure explicit.
Compile and materialize the small truth layout · 1:04
Compile the policy once, then materialize rows authenticated-owner and columns administrator-suspended. In false-first order, the first two rows are all zero because authentication is absent. Only three of the sixteen complete assignments are accepted. We will inspect why, rather than treating the matrix as a black box.
Trace an allowed administrator case · 1:26
Take authenticated one, owner zero, administrator one, suspended zero. Owner OR administrator gives one. Authentication is present and suspension is absent, so the final result is one. This is row one-zero and column one-zero, or row two and column two in binary addressing.
Change one fact: suspension · 1:47
Keep that same administrator case, but change suspended to one. The first two requirements still pass, but not suspended is now zero. The whole conjunction becomes zero. The highlighted cell moves one column to the right and changes from allow to deny.
Validate the policy exhaustively · 2:05
Our separate scalar oracle evaluates authenticated AND owner-or-administrator AND not-suspended for every four-bit assignment. Every matrix lookup matches. Three cases are allowed: authenticated, not suspended, and at least one of owner or administrator. The other thirteen are denied.
Your turn: does ownership override suspension? · 2:26
Suppose the person is authenticated and is the owner, is not an administrator, and is suspended. Should the policy allow access? Use the expression as written, not a different policy you might prefer. Identify which requirement decides the result.
Prediction pause: 8 seconds.
Answer: suspension still denies access · 2:50
The not-suspended factor is zero, so the result is deny even for an authenticated owner. If ownership were meant to override suspension, that would be a different policy expression requiring new tests. This example implements the stated rule, not a universal access-control design.
Retain what makes the result reproducible · 3:09
Keep the expression, variable map, axis ordering, compiled representation when useful, and validation results. This local example makes no deployment or security claim and no benchmark claim. Across the series, the same habit has mattered: define the object, show the operation, and verify the result against its meaning.

