Rendering a phase list's contracts as a table

Presentation only: it reads the phases' declared contracts and formats them, so it needs the phase vocabulary and nothing from the verifier.

Rendering a pipeline's contracts as a table

phaseTable renders a phase list as a dependency table: one numbered row per phase in run order, one column per fact, each cell a lifeline symbol read against the facts holding at that point in the pipeline. entryFacts seeds the facts assumed to hold on entry; a consumer (a name and the facts it requires, e.g. the verification back end) becomes a final requirements-only row. Unlike the composition checker, the walk does not stop at the first unmet requirement — it treats each as satisfied and carries on — so every breakage shows at once.

def Core.phaseTable (phases : List PipelinePhase) (entryFacts : ProgramFactSet := ProgramFactSet.empty) (consumer : Option (String × ProgramFactSet) := none) : String

Render phases as the dependency table. See the section comment.

Equations

• One or more equations did not get rendered due to their size.