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 EvalCommandE step.
• Procedure.checkAsPredicate_of_exprEq — transfers the reading of a captured check to another clause with the same expression.
• assertionsValid_defaultAssertEvents — turns non-free contract clauses that hold in every world into a valid assertion-event trace.
• Procedure.inputAsPredicate_int — an int input holds an integer at a well-formed entry satisfying the input typing.

theorem Core.Logic.Hoare.assertionsValid_defaultAssertEvents (conditionInterp : Imperative.ConditionInterp Expression) (fac : Expression.Factory) (σ : CoreStore) (checks : ListMap CoreLabel Procedure.Check) (h : ∀ (label : CoreLabel) (check : Procedure.Check), (label, check) ∈ checks.toList → check.attr = Procedure.CheckAttr.Default → ∀ (world : conditionInterp.World), conditionInterp.holds world { factory := fac, store := σ, label := label, expr := check.expr, metadata := check.md }) : Imperative.Trace.AssertionsValid Expression conditionInterp (defaultAssertEvents fac σ checks)

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

theorem Core.Logic.Hoare.Procedure.checkAsPredicate_of_exprEq {factory : Lambda.Factory CoreLParams} {ρ : Imperative.Env Expression} {label' : CoreLabel} {check' : Procedure.Check} (label : CoreLabel) (check : Procedure.Check) (hfac : ρ.factory.factory = factory) (hexpr : check'.expr = check.expr) (h : checkAsPredicate factory ρ label' check') : checkAsPredicate factory ρ label check

Transfer the reading of a captured check to another clause with the same expression, given that the environment's runtime factory is over factory.

theorem Core.Logic.Hoare.Procedure.contractTriple_of (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (bss : Statements) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured bss) (hchecksTyped : contractChecksTyped proc) (h : Triple p.findProcByString? params (preAsPredicate (p.factoryBeforeProcedure procName) proc) [Imperative.Stmt.block "" bss #[]] (contractPost (p.factoryBeforeProcedure procName) proc) (p.factoryBeforeProcedure procName)) : 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 only the preconditions.

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

Build a contractTriple whose body proof may assume the concrete factory and old-inout relation but does not need runtime input-value typing. The separate hchecksTyped argument discharges contractTriple's static requirement that each contract clause type-check as bool.

theorem Core.Logic.Hoare.Procedure.contractTriple_of_core_typed (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (bss : Statements) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured bss) (hchecksTyped : contractChecksTyped proc) (h : Triple p.findProcByString? params (contractPre (p.factoryBeforeProcedure procName) proc) [Imperative.Stmt.block "" bss #[]] (contractPost (p.factoryBeforeProcedure procName) proc) (p.factoryBeforeProcedure procName)) : 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 (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured []) (hchecksTyped : contractChecksTyped proc) (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.

theorem Core.Logic.Hoare.Procedure.contractTriple_nil_of_ensuresAmongRequires (p : Program) (params : InitEnvWFParams) (procName : String) (proc : Procedure) (hproc : p.findProcByString? procName = some proc) (hbody : proc.body = Imperative.Body.structured []) (hchecksTyped : contractChecksTyped proc) (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 (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]) (hchecksTyped : contractChecksTyped proc) (hsem : ∀ (ρ₀ : Imperative.Env Expression) (σ' : CoreStore) (emitted : Imperative.Trace Expression), contractPre (p.factoryBeforeProcedure procName) proc ρ₀ → InitEnvWF params (Imperative.Stmt.cmd c) ρ₀ → EvalCommandE p.findProcByString? ρ₀.factory ρ₀.store c σ' emitted → Imperative.Trace.AssertionsValid Expression (DenoteBasedInterp (p.factoryBeforeProcedure procName)) emitted ∧ (Imperative.Trace.Reachable Expression (DenoteBasedInterp (p.factoryBeforeProcedure procName)) emitted → contractPost (p.factoryBeforeProcedure procName) proc { store := σ', factory := ρ₀.factory })) (hpost_proj : Imperative.Logic.Hoare.PostWF [Imperative.Stmt.cmd c] (contractPost (p.factoryBeforeProcedure procName) 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.

theorem Core.Logic.Hoare.Procedure.inputAsPredicate_int {proc : Procedure} {ρ : Imperative.Env Expression} (hwf : Imperative.WellFormedStore ρ.store ρ.factory) (hin : inputAsPredicate proc ρ) (x : Expression.Ident) (hx : (x, Lambda.LMonoTy.int) ∈ ListMap.toList proc.header.inputs) : ∃ (k : Int), ρ.store x = some (Lambda.SemValue.ofInt ρ.factory.model.tcInterp k)

An input of type int holds an integer of the runtime factory at an entry with a well-formed store satisfying the procedure's input typing.