Phase contracts and validated pipelines #
The composition check, independent of any language. A phase is anything with a
name and three fact sets (PhaseContract); a ValidatedPipeline is a list of
them whose contracts line up, indexed by the facts it assumes of the program it
is given.
Nothing here knows what a phase does: the transform, the monad it runs in, and whatever else a language attaches to a phase stay on that language's side. What is shared is the part worth sharing — threading facts through a phase, deciding whether a list composes, and explaining why it does not.
Sets, derived #
The algebra supplies ofList and toList; everything the check needs follows
from them, so a representation has two operations to implement rather than ten.
The facts of a set, in the representation's order.
Equations
Instances For
Build a set from a list.
Instances For
Equations
- Strata.Pipeline.instMembershipFactSet = { mem := fun (σ : Strata.Pipeline.FactSet F) (f : F) => f ∈ Strata.Pipeline.factsOf σ }
The theorem below is stated here rather than with the other theorems about fact sets, because the decidable-equality instance that follows it is built from it. A properties module imports its definition module, so a definition cannot depend on a theorem stated there.
Extensionally equal fact sets are equal, which is what lets a set index a validated pipeline.
Equations
- Strata.Pipeline.instDecidableEqFactSet σ₁ σ₂ = decidable_of_iff (∀ (f : F), f ∈ Strata.Pipeline.FactVocabulary.all → (f ∈ σ₁ ↔ f ∈ σ₂)) ⋯
Nothing is known about the program.
Instances For
Every fact. The honest preserves for a phase that returns the program it
was given, and the only place a fact set may follow the vocabulary's
enumeration instead of being written out: a phase that changes nothing
preserves a new fact the moment the fact exists.
Equations
Instances For
Union: the facts of either set. The representation supplies it, so for the canonical list this is one walk of the vocabulary and the two sets.
Equations
Instances For
Intersection: the facts of both sets, by the same walk as union.
Equations
Instances For
Inclusion: used by the composition check, where the next phase's requires
must be covered by what the pipeline already guarantees. Decided by
FactAlgebra.decSubset, which for the canonical list is one walk of the two
sets — see canon_subset_iff_sublist.
It runs once per phase when a pipeline is checked.
Marked @[expose] so the body unfolds in importing modules: an inclusion
proof has to be applicable as a function.
Equations
- (σ₁ ⊑ σ₂) = ∀ (f : F), f ∈ Strata.Pipeline.factsOf σ₁ → f ∈ σ₂
Instances For
Equations
Inclusion: used by the composition check, where the next phase's requires
must be covered by what the pipeline already guarantees. Decided by
FactAlgebra.decSubset, which for the canonical list is one walk of the two
sets — see canon_subset_iff_sublist.
It runs once per phase when a pipeline is checked.
Marked @[expose] so the body unfolds in importing modules: an inclusion
proof has to be applicable as a function.
Equations
- Strata.Pipeline.«term_⊑_» = Lean.ParserDescr.trailingNode `Strata.Pipeline.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))
Instances For
Threading facts through a phase #
After a phase runs, the facts it establishes together with the facts in
σ that it preserves. Anything in neither is dropped.
Equations
- Strata.Pipeline.applyPhase establishes preserves σ = Strata.Pipeline.factSetUnion establishes (Strata.Pipeline.factSetInter σ preserves)
Instances For
Contracts #
What the validator needs of a phase: a name for diagnostics and the three fact sets of its contract. One instance per phase type.
- name : P → String
Canonical name of the phase, used in diagnostics.
- requires : P → FactSet F
Facts that must hold on the input program for this phase to run.
- establishes : P → FactSet F
Facts guaranteed to hold on the output program.
- preserves : P → FactSet F
Facts that, if they held on the input, also hold on the output.
Instances
Validated pipelines #
A pipeline validated to compose correctly, indexed by the facts it expects
at entry. What it establishes is not a second index but a function of this
one and the phases, computed by ValidatedPipeline.establishes.
cons p h rest runs p first and rest afterwards: h is about the facts
known on entry, which is why the head is the phase that receives the input
program and nil is the end of the run.
- nil {P F : Type} [FactVocabulary F] [FactAlgebra F] [PhaseContract P F] {requires : FactSet F} : ValidatedPipeline P F requires
- cons {P F : Type} [FactVocabulary F] [FactAlgebra F] [PhaseContract P F] {requires : FactSet F} (p : P) (h : PhaseContract.requires p ⊑ requires) (rest : ValidatedPipeline P F (applyPhase (PhaseContract.establishes p) (PhaseContract.preserves p) requires)) : ValidatedPipeline P F requires
Instances For
What the pipeline establishes of the program it produces, given that its own
requires held of the program it was given: the requires carried through
applyPhase by every phase in turn.
The same relation to requires that a phase's establishes has to its own,
which is why it takes that name. It is derived rather than declared, so there
is nowhere to state it wrongly.
Equations
Instances For
The phases of this pipeline, in the order they run.
Equations
- Strata.Pipeline.ValidatedPipeline.nil.phases = []
- (Strata.Pipeline.ValidatedPipeline.cons p h rest).phases = p :: rest.phases
Instances For
Checking a phase list #
Pipelines are assembled and checked at runtime. Because ⊑ is decidable,
checking a phase list produces the per-phase inclusion proof instead of
demanding one.
The facts needed asks for that σ does not supply. Empty exactly when
needed ⊑ σ.
Equations
- Strata.Pipeline.missingFacts needed σ = List.filter (fun (x : F) => decide ¬x ∈ σ) (Strata.Pipeline.factsOf needed)
Instances For
Tracing a lost fact #
A rejection says where the missing fact came from and which phase dropped it, so
the author knows what to reorder. The walked prefix is threaded as
(position, phase) pairs together with the caller's entry facts, which is what
those two ends are read off. A fact can enter either way — established by a
phase, or supplied by the caller — so the origin is a phase position or entry
at position 0.
Validate a dynamically assembled phase list against the facts σ known to
hold on entry. On failure, an explanatory diagnostic for the first phase
whose contract is unmet; positions in diagnostics are 1-based.
Equations
- Strata.Pipeline.ValidatedPipeline.ofListFrom σ phases = Strata.Pipeline.ValidatedPipeline.ofListAux✝ σ σ [] phases
Instances For
Validate a phase list that assumes nothing about its input program.
Equations
Instances For
Validate phases against facts σ₀ assumed to hold on the input program, and
that what they establish covers what consumer needs of the program they
produce. The result is indexed by σ₀, so a caller must supply a proof that
σ₀ holds of the program it hands to the pipeline.
The consumer is not a phase — it hands on no program — so it is not modelled as one; it is reported through the same diagnostic, at the position after the last phase.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ofListFromDelivering for a phase list that assumes nothing about its input
program.
Equations
- Strata.Pipeline.ValidatedPipeline.ofListDelivering consumer needed phases = Strata.Pipeline.ValidatedPipeline.ofListFromDelivering Strata.Pipeline.emptyFactSet consumer needed phases