Discharging a procedure's contract

Ways to establish a Procedure.contractTriple, and the bridges that make a concrete procedure's contract decidable. The definitions being established live in Strata.Languages.Core.Logic.ContractToHoareTriple.

Key results

• Procedure.contractTriple_of — supplies the procedure and body, discharging the name lookup and the .structured obligation once.
• Procedure.contractTriple_of_core and Procedure.contractTriple_of_core_typed — retain the concrete Core entry facts needed by evaluator-sensitive body proofs.
• Procedure.contractTriple_nil and Procedure.contractTriple_nil_of_ensuresAmongRequires — an empty body meets a contract whose non-free ensures clauses are all among its requires.
• Procedure.contractTriple_singleton_cmd — a one-command body, reduced to a single obligation about that command's EvalCommand step.
• Procedure.preAsPredicate_of_preHoldsAt and Procedure.not_postAsPredicate_of_postRefutedAt — the decidable bridges, which let a concrete procedure be settled by decide / native_decide rather than by unfolding a translated AST by hand.
• preAsPredicate_of_eqPairs and postAsPredicate_of_eqPairs — establish contract clauses that are equalities between variables with matching canonical bindings.
• assertionsValid_defaultAssertEvents — turns true non-free contract clauses into a valid assertion-event trace.

theorem Core.Logic.Hoare.assertionsValid_defaultAssertEvents (fac : Expression.Factory) (σ : CoreStore) (checks : ListMap CoreLabel Procedure.Check) (h : ∀ (label : CoreLabel) (check : Procedure.Check), (label, check) ∈ checks.toList → check.attr = Procedure.CheckAttr.Default → Expression.eval fac σ check.expr = some Imperative.HasBool.tt) : Imperative.Trace.AssertionsValid Expression (Imperative.EvaluatorBasedInterp Expression) (defaultAssertEvents fac σ checks)

A snapshot of a procedure's non-free contract clauses as assert events is assertion-valid whenever every such clause evaluates to true in that snapshot.

theorem Core.Logic.Hoare.preAsPredicate_of_eqPairs (proc : Procedure) (ρ : Imperative.Env Expression) (pairs : List ((Expression.Ident × Option Lambda.LMonoTy) × Expression.Ident × Option Lambda.LMonoTy)) (hsyn : (proc.spec.preconditions.toList.all fun (lc : String × Imperative.Check Expression) => pairs.any fun (p : (Expression.Ident × Option Lambda.LMonoTy) × Expression.Ident × Option Lambda.LMonoTy) => decide (lc.snd.expr = Lambda.LExpr.eq () (Lambda.LExpr.fvar () p.fst.fst p.fst.snd) (Lambda.LExpr.fvar () p.snd.fst p.snd.snd))) = true) (hstore : ∀ (p : (Expression.Ident × Option Lambda.LMonoTy) × Expression.Ident × Option Lambda.LMonoTy), p ∈ pairs → ∃ (v : Expression.Expr), ρ.store p.fst.fst = some v ∧ ρ.store p.snd.fst = some v ∧ Lambda.LExpr.isCanonicalValue ρ.factory v = true) : Procedure.preAsPredicate proc ρ

If every requires is an equality between a listed variable pair whose two bindings hold the same canonical value, all preconditions hold.

theorem Core.Logic.Hoare.postAsPredicate_of_eqPairs (proc : Procedure) (ρ : Imperative.Env Expression) (pairs : List ((Expression.Ident × Option Lambda.LMonoTy) × Expression.Ident × Option Lambda.LMonoTy)) (hsyn : (proc.spec.postconditions.toList.all fun (lc : String × Imperative.Check Expression) => decide (lc.snd.attr ≠ Procedure.CheckAttr.Default) || pairs.any fun (p : (Expression.Ident × Option Lambda.LMonoTy) × Expression.Ident × Option Lambda.LMonoTy) => decide (lc.snd.expr = Lambda.LExpr.eq () (Lambda.LExpr.fvar () p.fst.fst p.fst.snd) (Lambda.LExpr.fvar () p.snd.fst p.snd.snd))) = true) (hstore : ∀ (p : (Expression.Ident × Option Lambda.LMonoTy) × Expression.Ident × Option Lambda.LMonoTy), p ∈ pairs → ∃ (v : Expression.Expr), ρ.store p.fst.fst = some v ∧ ρ.store p.snd.fst = some v ∧ Lambda.LExpr.isCanonicalValue ρ.factory v = true) : Procedure.postAsPredicate proc ρ

Postcondition analogue of preAsPredicate_of_eqPairs: free clauses are exempt, and each remaining equality follows from matching canonical bindings.

theorem Core.Logic.Hoare.Procedure.contractTriple_of (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (bss : Statements) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured bss) (h : Triple p.findProcByString? φ params (preAsPredicate proc) [Imperative.Stmt.block "" bss #[]] (postAsPredicate proc)) : contractTriple φ p params procName

Build a contractTriple from the name lookup, body, and body judgement. The factory, old-inout, and input-typing clauses of contractTriple's precondition are discarded by weakening, so the body proof needs none of them.

theorem Core.Logic.Hoare.Procedure.contractTriple_of_core (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (bss : Statements) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured bss) (h : Triple p.findProcByString? φ params (fun (ρ : Imperative.Env Expression) => preAsPredicate proc ρ ∧ ρ.factory = Factory ∧ oldInoutAsPredicate proc ρ) [Imperative.Stmt.block "" bss #[]] (postAsPredicate proc)) : contractTriple φ p params procName

Build a contractTriple whose body proof may assume the concrete factory and old-inout relation but does not need input-value typing.

theorem Core.Logic.Hoare.Procedure.contractTriple_of_core_typed (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (bss : Statements) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured bss) (h : Triple p.findProcByString? φ params (fun (ρ : Imperative.Env Expression) => preAsPredicate proc ρ ∧ ρ.factory = Factory ∧ oldInoutAsPredicate proc ρ ∧ inputAsPredicate proc ρ) [Imperative.Stmt.block "" bss #[]] (postAsPredicate proc)) : contractTriple φ p params procName

Build a contractTriple while retaining every entry fact, including values matching the types of the procedure's input and inout formals.

theorem Core.Logic.Hoare.Procedure.contractTriple_nil (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured []) (himp : ∀ (label : CoreLabel) (check : Procedure.Check), (label, check) ∈ proc.spec.postconditions.toList → check.attr = Procedure.CheckAttr.Default → ∃ (label' : CoreLabel), ∃ (check' : Procedure.Check), (label', check') ∈ proc.spec.preconditions.toList ∧ check'.expr = check.expr) : contractTriple φ p params procName

A contract whose every non-free ensures is literally one of the requires is met by an empty body: nothing runs, so the precondition still holds at the end.

The workhorse is skip_block plus consequence; no reasoning about Expression.eval is involved, because the same check expression carries from the precondition to the postcondition.

theorem Core.Logic.Hoare.Procedure.preAsPredicate_of_preHoldsAt {proc : Procedure} {ρ : Imperative.Env Expression} (h : preHoldsAt proc ρ = true) : preAsPredicate proc ρ

The decidable check preHoldsAt discharges the proposition preAsPredicate.

theorem Core.Logic.Hoare.Procedure.not_postAsPredicate_of_postRefutedAt {proc : Procedure} {ρ : Imperative.Env Expression} (h : postRefutedAt proc ρ = true) : ¬postAsPredicate proc ρ

The decidable check postRefutedAt refutes the proposition postAsPredicate: the clause it finds is a non-free ensures that does not hold.

theorem Core.Logic.Hoare.Procedure.contractTriple_nil_of_ensuresAmongRequires (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured []) (h : ensuresAmongRequires proc = true) : contractTriple φ p params procName

An empty body meets a contract whose non-free ensures clauses are all among its requires, with the containment settled by the decidable ensuresAmongRequires.

theorem Core.Logic.Hoare.Procedure.contractTriple_singleton_cmd (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (hproc : p.findProcByString? procName = some proc) (c : Command) (hbody : proc.body = Imperative.Body.structured [Imperative.Stmt.cmd c]) (hsem : ∀ (ρ₀ : Imperative.Env Expression) (σ' : CoreStore) (emitted : Imperative.Trace Expression), preAsPredicate proc ρ₀ → ρ₀.factory = Factory → oldInoutAsPredicate proc ρ₀ → InitEnvWF params (Imperative.Stmt.cmd c) ρ₀ → EvalCommandE p.findProcByString? φ ρ₀.factory ρ₀.store c σ' emitted → Imperative.Trace.AssertionsValid Expression (Imperative.EvaluatorBasedInterp Expression) emitted ∧ (Imperative.Trace.Reachable Expression (Imperative.EvaluatorBasedInterp Expression) emitted → postAsPredicate proc { store := σ', factory := ρ₀.factory, hasFailure := ρ₀.hasFailure })) (hpost_proj : Imperative.Logic.Hoare.PostWF [Imperative.Stmt.cmd c] (postAsPredicate proc)) : contractTriple φ p params procName

A one-command body. The cmd rule reduces a contract over [.cmd c] to a single semantic obligation about c. hsem receives the precondition clauses, concrete factory, and old-inout relation; signature typing is weakened away because this constructor does not require it. hpost_proj ensures the postcondition names no variable declared by c, since the block drops those.