Module receipt 

The stages a Lean → LOGOS result passes through, named separately so that no result is ever one unexplained “verified” Boolean (competition rule R1). The names are the contract’s wire names.

Structs

Receipt

A receipt: one entry per stage in STAGES, in order. Verified only when every stage passed.

Stage

Enums

StageStatus

What happened in one stage. NotRun and Unsupported are never a pass.

Constants

REPLAY_STAGES

The stages a replay establishes from a package’s bytes alone. lean_accepted is not among them: a replay never runs Lean, and says so rather than inheriting the producing run’s word.

STAGES

Every stage, in the order a result passes through them.