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. The rendering itself is Strata.Pipeline.lifelineTable, shared with every other pipeline that declares contracts; what belongs here is only the Core-specific part, namely how a ProgramFact earns its column label.

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.

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.