Skip to content

Capstone Proof Guide

Page Maps

graph LR
  family["Reproducible Research"]
  program["Deep Dive Make"]
  section["Capstone"]
  page["Capstone Proof Guide"]
  capstone["Capstone evidence"]

  family --> program --> section --> page
  page -.applies in.-> capstone
flowchart LR
  orient["Orient on the page map"] --> read["Read the main claim and examples"]
  read --> inspect["Inspect the related code, proof, or capstone surface"]
  inspect --> verify["Run or review the verification path"]
  verify --> apply["Apply the idea back to the module and capstone"]

Read the first diagram as a timing map: this guide is for one end-to-end proof pass, not for first contact. Read the second diagram as the rule: run the bounded proof route, inspect the evidence in order, then leave with one explicit judgment about trust.

Use this guide after Module 03, or later when you need a steward-level review route before incident, profile, or migration questions.

Bounded proof pass

  1. Run make PROGRAM=reproducible-research/deep-dive-make proof.
  2. Read Command Guide.
  3. Read capstone/Makefile and capstone/tests/run.sh.
  4. Inspect artifacts/proof/reproducible-research/deep-dive-make/selftest/.
  5. Inspect artifacts/audit/reproducible-research/deep-dive-make/contract/.
  6. Inspect artifacts/audit/reproducible-research/deep-dive-make/incident/.
  7. Inspect artifacts/audit/reproducible-research/deep-dive-make/profile/.
  8. If you still need failure-class study after the bounded proof route, step down into programs/reproducible-research/deep-dive-make/capstone/ and run gmake repro.

Questions this proof pass should answer

  • what selftest proves that all does not
  • where the public contract becomes inspectable
  • where hidden inputs and generated boundaries are made visible
  • which saved bundle would matter most to another maintainer
  • which repro teaches a real failure class instead of a toy surprise

Failure-study route

Use this route when the open question is about one failure class rather than the whole healthy build:

  1. Start with capstone/repro/01-shared-log.mk.
  2. Then inspect capstone/repro/05-mkdir-race.mk and capstone/repro/06-order-only-misuse.mk.
  3. State the defect class in words before proposing a repair.
  4. Return to capstone/tests/run.sh to compare the broken specimen with the healthy proof harness.

Good stopping point

Stop when you can write one explicit judgment in your own words:

  • trust the build contract as-is
  • trust it with one named boundary to revisit
  • do not trust it yet because one specific proof surface is still missing

If you cannot make one of those judgments, repeat the bounded route before adding more commands.

Best follow-up routes