Hoare Logic for Core

The structural Hoare rules of Imperative.Logic.Hoare, instantiated for Core directly over its own language of statement lists, EventLang.coreBlock: there is a single judgement, Triple, conditioned on Core.Logic.BlockInitEnvWF.

Contents

Triple, and the rules false_pre, consequence, cmd, set, init, seq, exit_cons, block, skip, ite and while_rule.

Why the rules are here and not in a HoareProps module

As in Strata.DL.Imperative.Logic.HoareTemplate: the rules below are the logic rather than properties of it, so they stay with the judgements they introduce. What does live separately is the contract integration: ContractToHoareTriple defines the contract reading, ContractToHoareTripleProps discharges it, and HoareCall provides the rule for procedure calls.

The Core triple

def Core.Logic.Hoare.TripleWith (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (conditionInterp : Imperative.ConditionInterp Expression) (params : InitEnvWFParams) (Pre : Imperative.Env Expression → Prop) (ss : Statements) (Post : Imperative.Env Expression → Prop) : Prop

Core Hoare triple with an explicit event-condition interpretation.

Equations

• Core.Logic.Hoare.TripleWith π φ conditionInterp params Pre ss Post = Strata.Logic.Hoare.TripleWith (Core.Logic.EventLang.coreBlock π φ) conditionInterp params Pre ss Post

def Core.Logic.Hoare.Triple (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) (Pre : Imperative.Env Expression → Prop) (ss : Statements) (Post : Imperative.Env Expression → Prop) : Prop

Core Hoare triple over statement lists.

Equations

• Core.Logic.Hoare.Triple π φ params Pre ss Post = Core.Logic.Hoare.TripleWith π φ (Imperative.EvaluatorBasedInterp Core.Expression) params Pre ss Post

Parametric rules

theorem Core.Logic.Hoare.false_pre (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) (ss : Statements) (Post : Imperative.Env Expression → Prop) : Triple π φ params (fun (x : Imperative.Env Expression) => False) ss Post

False precondition proves anything.

theorem Core.Logic.Hoare.consequence (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) {Pre Pre' Post Post' : Imperative.Env Expression → Prop} {ss : Statements} (h : Triple π φ params Pre ss Post) (hpre : ∀ (ρ : Imperative.Env Expression), Pre' ρ → Pre ρ) (hpost : ∀ (ρ : Imperative.Env Expression), Post ρ → Post' ρ) : Triple π φ params Pre' ss Post'

Consequence (weakening): strengthen the precondition, weaken the postcondition.

Rules for a single command

theorem Core.Logic.Hoare.cmd (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) (c : Command) (Pre Post : Imperative.Env Expression → Prop) (h : ∀ (ρ₀ : Imperative.Env Expression) (σ' : CoreStore) (emitted : Imperative.Trace Expression), Pre ρ₀ → InitEnvWF params (Imperative.Stmt.cmd c) ρ₀ → EvalCommandE π φ ρ₀.factory ρ₀.store c σ' emitted → Imperative.Trace.AssertionsValid Expression (Imperative.EvaluatorBasedInterp Expression) emitted ∧ (Imperative.Trace.Reachable Expression (Imperative.EvaluatorBasedInterp Expression) emitted → Post { store := σ', factory := ρ₀.factory, hasFailure := ρ₀.hasFailure })) : Triple π φ params Pre [Imperative.Stmt.cmd c] Post

A generic single Core command. h receives the full InitEnvWF params (.cmd c) ρ₀, including the WellFormedSemanticEval bundle that EvalCommandE needs.

theorem Core.Logic.Hoare.set (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) (x : Expression.Ident) (e : Expression.Expr) (md : Imperative.MetaData Expression) (Pre Post : Imperative.Env Expression → Prop) (hpost : ∀ (ρ₀ : Imperative.Env Expression) (σ' : CoreStore) (v : Expression.Expr), Pre ρ₀ → Expression.eval ρ₀.factory ρ₀.store e = some v → Imperative.UpdateState Expression ρ₀.store x v σ' → Post { store := σ', factory := ρ₀.factory, hasFailure := ρ₀.hasFailure }) : Triple π φ params Pre [Statement.set x e md] Post

Assignment. The value written is quantified inside hpost, next to the evaluation that produced it: which value e takes depends on the environment, so fixing one outside would demand that Pre determine it.

theorem Core.Logic.Hoare.init (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) (x : Expression.Ident) (ty : Expression.Ty) (e : Expression.Expr) (md : Imperative.MetaData Expression) (Pre Post : Imperative.Env Expression → Prop) (hpost : ∀ (ρ₀ : Imperative.Env Expression) (σ' : CoreStore) (v : Expression.Expr), Pre ρ₀ → Expression.eval ρ₀.factory ρ₀.store e = some v → Imperative.InitState Expression ρ₀.store x v σ' → Post { store := σ', factory := ρ₀.factory, hasFailure := ρ₀.hasFailure }) : Triple π φ params Pre [Statement.init x ty (Imperative.ExprOrNondet.det e) md] Post

Declaration. InitState differs from UpdateState only in requiring the slot to have been undefined beforehand, which the postcondition never inspects.

Structural rules

theorem Core.Logic.Hoare.seq (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) {ss₁ ss₂ : Statements} {Pre Mid Post : Imperative.Env Expression → Prop} (hnofd : Imperative.Block.noFuncDecl ss₁ = true) (h₁ : Triple π φ params Pre ss₁ Mid) (h₂ : Triple π φ params Mid ss₂ Post) (hnoesc : Imperative.Block.exitsCoveredByBlocks [] ss₁) : Triple π φ params Pre (ss₁ ++ ss₂) Post

Sequencing: glue two triples along the concatenation of their statement lists. hnofd keeps the factory constant across the prefix's run, which is what lets the well-formedness condition be re-established on the suffix; see Imperative.Logic.Hoare.seq_append for why hnoesc is needed.

theorem Core.Logic.Hoare.exit_cons (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) {lbl : String} {md : Imperative.MetaData Expression} {ss : Statements} (Pre : Imperative.Env Expression → Prop) : Triple π φ params Pre (Imperative.Stmt.exit lbl md :: ss) Pre

An exit ends the statement list where it stands, leaving the environment untouched, so the precondition survives to the exiting configuration. The statements after it never run. An enclosing block catches the exit.

theorem Core.Logic.Hoare.block (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) {ss : Statements} {l : String} {md : Imperative.MetaData Expression} {Pre Post : Imperative.Env Expression → Prop} (hnofd : Imperative.Block.noFuncDecl ss = true) (h : Triple π φ params Pre ss Post) (hpost_proj : Imperative.Logic.Hoare.PostWF ss Post) : Triple π φ params Pre [Imperative.Stmt.block l ss md] Post

Wrap a statement list in a labelled block. Post must not mention the names the body scopes (PostWF), and hnofd keeps the factory constant across the body, so leaving the block restores nothing.

theorem Core.Logic.Hoare.skip (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) (l : String) (md : Imperative.MetaData Expression) (Pre : Imperative.Env Expression → Prop) : Triple π φ params Pre [Imperative.Stmt.block l [] md] Pre

Empty block is skip. No lowering condition: the generic rule instantiates skip_block at the trivial block condition.

theorem Core.Logic.Hoare.ite (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) {cond : Expression.Expr} {tss ess : Statements} {md : Imperative.MetaData Expression} {Pre Post : Imperative.Env Expression → Prop} (hnofd : (Imperative.Stmt.ite (Imperative.ExprOrNondet.det cond) tss ess md).noFuncDecl = true) (ht : Triple π φ params (fun (ρ : Imperative.Env Expression) => Pre ρ ∧ Expression.eval ρ.factory ρ.store cond = some Imperative.HasBool.tt) tss Post) (he : Triple π φ params (fun (ρ : Imperative.Env Expression) => Pre ρ ∧ Expression.eval ρ.factory ρ.store cond = some Imperative.HasBool.ff) ess Post) (hthen_proj : Imperative.Logic.Hoare.PostWF tss Post) (helse_proj : Imperative.Logic.Hoare.PostWF ess Post) : Triple π φ params Pre [Imperative.Stmt.ite (Imperative.ExprOrNondet.det cond) tss ess md] Post

If-then-else rule.

theorem Core.Logic.Hoare.while_rule (π : String → Option Procedure) (φ : Expression.Factory → Imperative.PureFunc Expression → Expression.Factory) (params : InitEnvWFParams) {guard : Expression.Expr} {measure : Option Expression.Expr} {inv : List (String × Expression.Expr)} {body : Statements} {md : Imperative.MetaData Expression} {Inv : Imperative.Env Expression → Prop} (hnofd : Imperative.Block.noFuncDecl body = true) (hbody : Triple π φ params (fun (ρ : Imperative.Env Expression) => Inv ρ ∧ Expression.eval ρ.factory ρ.store guard = some Imperative.HasBool.tt) body Inv) (hcov : Imperative.Block.exitsCoveredByBlocks [] body) (hInv_proj : Imperative.Logic.Hoare.PostWF body Inv) : Triple π φ params Inv [Imperative.Stmt.loop (Imperative.ExprOrNondet.det guard) measure inv body md] fun (ρ : Imperative.Env Expression) => Inv ρ ∧ Expression.eval ρ.factory ρ.store guard = some Imperative.HasBool.ff

While rule. hcov says the body's exits are all caught inside the body, and hInv_proj that the invariant survives the body block's store projection.