Core structured-to-unstructured pipeline properties

Cross-pass precondition facts for the Core pipeline s2uPipeline, consumed by StructuredToUnstructuredPipelineCoreCorrect.

Key results:

• Core.StructuredToUnstructuredPipeline.nondetElim_establishes_hoistPre — a nondetElim output of a block satisfying the pipeline source condition satisfies the loop-init hoist input condition.
• Core.StructuredToUnstructuredPipeline.hoist_establishes_loweringPre — a successful Core loop-init hoist maps that condition to the stmtsToCFG input condition.

Core cross-pass precondition implications

The Core pipeline correctness theorem exposes its complete source precondition directly. These implications connect that visible source condition to the next pass's visible condition; neither hides the pipeline precondition behind a named predicate.

theorem Core.StructuredToUnstructuredPipeline.nondetElim_establishes_hoistPre (ss out : List (Imperative.Stmt Expression Command)) : (fun (ss : List (Imperative.Stmt Expression Command)) => some (Imperative.Block.nondetElim ss)) ss = some out → (Statements.noCalls ss = true ∧ Imperative.Block.loopHasNoInvariants ss = true ∧ Imperative.Block.noMeasureLoops ss = true ∧ Imperative.Block.uniqueInits ss ∧ Imperative.Block.exitsCoveredByBlocks [] ss ∧ Imperative.Block.userLabelsShapeNodup ss ∧ ∀ (name : String), Imperative.NondetElim.isGeneratedName name → ¬Imperative.HasIdent.ident name ∈ Imperative.Block.definedVars ss false ++ Imperative.Block.modifiedVars ss) → Statements.noCalls out = true ∧ Imperative.Block.noNondetGuards out = true ∧ Imperative.Block.uniqueInits out ∧ Imperative.Block.loopHasNoInvariants out = true ∧ Imperative.Block.noMeasureLoops out = true ∧ Imperative.Block.exitsCoveredByBlocks [] out ∧ Imperative.Block.userLabelsShapeNodup out

A Core Block.nondetElim output satisfies the strengthened hoist input condition used by the pipeline.

theorem Core.StructuredToUnstructuredPipeline.hoist_establishes_loweringPre (ss out : Statements) : hoistLoopPrefixInits ss = some out → ss.noCalls = true ∧ Imperative.Block.noNondetGuards ss = true ∧ Imperative.Block.uniqueInits ss ∧ Imperative.Block.loopHasNoInvariants ss = true ∧ Imperative.Block.noMeasureLoops ss = true ∧ Imperative.Block.exitsCoveredByBlocks [] ss ∧ Imperative.Block.userLabelsShapeNodup ss → out.noCalls = true ∧ Imperative.Block.noNondetGuards out = true ∧ Imperative.Block.uniqueInits out ∧ Imperative.Block.loopBodyNoInits out = true ∧ Imperative.Block.loopHasNoInvariants out = true ∧ Imperative.Block.noMeasureLoops out = true ∧ Imperative.Block.exitsCoveredByBlocks [] out ∧ Imperative.Block.userLabelsShapeNodup out

A successful Core loop-init hoist maps the strengthened pipeline hoist condition to the complete visible stmtsToCFG condition.