Skip to content

Walkthrough Guide

Guide Maps

graph LR
  family["Reproducible Research"]
  program["Deep Dive Make"]
  guide["Capstone docs"]
  section["Docs"]
  page["Walkthrough Guide"]
  proof["Proof route"]

  family --> program --> guide --> section --> page
  page -.checks against.-> proof
flowchart LR
  orient["Read the guide boundary"] --> inspect["Inspect the named files, targets, or artifacts"]
  inspect --> run["Run the confirm, demo, selftest, or proof command"]
  run --> compare["Compare output with the stated contract"]
  compare --> review["Return to the course claim with evidence"]

Use this guide for first contact with the capstone. It keeps the first pass bounded and human-readable, so you do not have to choose between random browsing and the strongest route in the repository.

  1. run make walkthrough
  2. read README.md to understand what this repository is trying to prove
  3. read TARGET_GUIDE.md to learn the public target surface
  4. read PROOF_GUIDE.md to see how claims map to evidence
  5. read tests/run.sh to understand what the proof harness actually checks
  6. read ARCHITECTURE.md and mk/contract.mk to place ownership and platform boundaries
  7. inspect repro/01-shared-log.mk to see one failure class in miniature

That route keeps claim first, proof second, ownership third, and controlled failure last.

If you have 15 minutes

Read:

Outcome: you should be able to name the public surface and the next target you would run.

If you have 45 minutes

Read:

Outcome: you should understand what the capstone proves and where boundary decisions live.

If you have 90 minutes

Read:

  • the 45-minute route
  • mk/objects.mk
  • mk/stamps.mk
  • REPRO_GUIDE.md
  • repro/01-shared-log.mk

Outcome: you should be able to explain graph truth, modeled hidden inputs, and one failure class without hand-waving.

Questions to keep asking

  • what is this repository claiming right now
  • which target is the smallest honest route for that claim
  • which file owns the rule, and which file proves it
  • where would a hidden input become visible if the graph stopped telling the truth
  • which failure specimen would teach this concept faster than more prose

Exit criteria

The walkthrough has done its job if you can answer these without guessing:

  • why selftest is stronger than all
  • when to choose inspect instead of proof
  • which file declares the execution boundary
  • which repro you would use to show a concurrency defect to another engineer