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, of_storeWF_pre, of_forall_entryFactory, cmd, set, init, init_nondet, havoc, assume, assume_eval, assert, assert_eval, 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 denotational domain of Core real is Strata.Util.Real, inherited from Lambda.SortDenote, so these Hoare judgements state correctness over the real numbers.

The Core triple

def Core.Logic.Hoare.TripleWith (π : String → Option Procedure) (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) (params : InitEnvWFParams) (Pre : Imperative.Env Expression → Prop) (ss : Statements) (Post : Imperative.Env Expression → Prop) (factory : Lambda.Factory CoreLParams := Factory) : Prop

Core Hoare triple over statement lists, with conditions read by evaluation in runtime factories over factory (DenoteBasedInterp factory). A runtime factory carries a model of factory, so the triple covers every model through the entry environments it quantifies over. The default is Core.Factory; program-level clients can supply the factory visible at a particular declaration.

Equations

• Core.Logic.Hoare.Triple π params Pre ss Post factory = Core.Logic.Hoare.TripleWith π (Core.Logic.DenoteBasedInterp factory) params Pre ss Post

Parametric rules

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

False precondition proves anything.

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

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

theorem Core.Logic.Hoare.of_storeWF_pre (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) {Pre Post : Imperative.Env Expression → Prop} {ss : Statements} (h : Triple π params (fun (ρ : Imperative.Env Expression) => Pre ρ ∧ Imperative.WellFormedStore ρ.store ρ.factory) ss Post factory) : Triple π params Pre ss Post factory

A triple whose precondition also requires a well-formed entry store holds without that requirement: the gate of every admitted entry gives it.

theorem Core.Logic.Hoare.of_forall_entryFactory (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) {Pre Post : Imperative.Env Expression → Prop} {ss : Statements} (h : ∀ (E : Expression.Factory), Triple π params (fun (ρ : Imperative.Env Expression) => Pre ρ ∧ ρ.factory = E) ss Post factory) : Triple π params Pre ss Post factory

A triple holds when it holds, for every runtime factory E, from the entries whose runtime factory is E.

Rules for a single command

theorem Core.Logic.Hoare.cmd (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (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 (DenoteBasedInterp factory) emitted ∧ (Imperative.Trace.Reachable Expression (DenoteBasedInterp factory) emitted → Post { store := σ', factory := ρ₀.factory })) : Triple π params Pre [Imperative.Stmt.cmd c] Post factory

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) {factory : Lambda.Factory CoreLParams} (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.Val), Pre ρ₀ → Expression.eval ρ₀.factory ρ₀.store e = some v → Imperative.UpdateState Expression ρ₀.store x v σ' → Post { store := σ', factory := ρ₀.factory }) : Triple π params Pre [Statement.set x e md] Post factory

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) {factory : Lambda.Factory CoreLParams} (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.Val), Pre ρ₀ → Expression.eval ρ₀.factory ρ₀.store e = some v → Imperative.InitState Expression ρ₀.store x v σ' → Post { store := σ', factory := ρ₀.factory }) : Triple π params Pre [Statement.init x ty (Imperative.ExprOrNondet.det e) md] Post factory

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

theorem Core.Logic.Hoare.init_nondet (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) (x : Expression.Ident) (ty : Expression.Ty) (md : Imperative.MetaData Expression) (Pre Post : Imperative.Env Expression → Prop) (hpost : ∀ (ρ₀ : Imperative.Env Expression) (σ' : CoreStore) (v : Expression.Val), Pre ρ₀ → Imperative.InitState Expression ρ₀.store x v σ' → Imperative.HasVal.valueOfTy ρ₀.factory v ty → Post { store := σ', factory := ρ₀.factory }) : Triple π params Pre [Statement.init x ty Imperative.ExprOrNondet.nondet md] Post factory

Declaration without an initial value. The variable is bound to an arbitrary value of its declared type, which is all the postcondition may rely on.

theorem Core.Logic.Hoare.havoc (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) (x : Expression.Ident) (md : Imperative.MetaData Expression) (Pre Post : Imperative.Env Expression → Prop) (hpost : ∀ (ρ₀ : Imperative.Env Expression) (σ' : CoreStore) (v : Expression.Val), Pre ρ₀ → Imperative.UpdateState Expression ρ₀.store x v σ' → Imperative.HasVal.valueOfStoredTy Expression ρ₀.factory ρ₀.store x v → Post { store := σ', factory := ρ₀.factory }) : Triple π params Pre [Statement.havoc x md] Post factory

Havoc. The variable takes an arbitrary value of the type of the value it held, which is all the postcondition may rely on.

theorem Core.Logic.Hoare.assume (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) (label : String) (e : Expression.Expr) (md : Imperative.MetaData Expression) (Pre Post : Imperative.Env Expression → Prop) (hpost : ∀ (ρ₀ : Imperative.Env Expression), Pre ρ₀ → (∃ (world : (DenoteBasedInterp factory).World), (DenoteBasedInterp factory).holds world { factory := ρ₀.factory, store := ρ₀.store, label := label, expr := e, metadata := md }) → Post ρ₀) : Triple π params Pre [Statement.assume label e md] Post factory

Assumption. The store is unchanged, and the postcondition is owed only where the assumed condition holds in some world: an assumption that cannot hold makes the rest of the run unreachable.

theorem Core.Logic.Hoare.assume_eval (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) (label : String) (e : Expression.Expr) (md : Imperative.MetaData Expression) (Pre Post : Imperative.Env Expression → Prop) (hfac : ∀ (ρ₀ : Imperative.Env Expression), Pre ρ₀ → ρ₀.factory.factory = factory) (hpost : ∀ (ρ₀ : Imperative.Env Expression), Pre ρ₀ → Expression.eval ρ₀.factory ρ₀.store e = some (Imperative.HasBool.ttVal ρ₀.factory) → Post ρ₀) : Triple π params Pre [Statement.assume label e md] Post factory

Assumption, where the precondition fixes the runtime factory to be over factory: the assumed condition then holds exactly when it evaluates to true.

theorem Core.Logic.Hoare.assert (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) (label : String) (e : Expression.Expr) (md : Imperative.MetaData Expression) (Pre : Imperative.Env Expression → Prop) (hvalid : ∀ (ρ₀ : Imperative.Env Expression), Pre ρ₀ → ∀ (world : (DenoteBasedInterp factory).World), (DenoteBasedInterp factory).holds world { factory := ρ₀.factory, store := ρ₀.store, label := label, expr := e, metadata := md }) : Triple π params Pre [Statement.assert label e md] Pre factory

Assertion. The store is unchanged, and the asserted condition must hold in every world at every environment the precondition admits.

theorem Core.Logic.Hoare.assert_eval (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) (label : String) (e : Expression.Expr) (md : Imperative.MetaData Expression) (Pre : Imperative.Env Expression → Prop) (hfac : ∀ (ρ₀ : Imperative.Env Expression), Pre ρ₀ → ρ₀.factory.factory = factory) (hvalid : ∀ (ρ₀ : Imperative.Env Expression), Pre ρ₀ → Expression.eval ρ₀.factory ρ₀.store e = some (Imperative.HasBool.ttVal ρ₀.factory)) : Triple π params Pre [Statement.assert label e md] Pre factory

Assertion, where the precondition fixes the runtime factory to be over factory: the asserted condition then holds exactly when it evaluates to true.

Structural rules

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

Sequencing: glue two triples along the concatenation of their statement lists. No statement step mutates the factory 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) {factory : Lambda.Factory CoreLParams} (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 factory

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) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) {ss : Statements} {l : String} {md : Imperative.MetaData Expression} {Pre Post : Imperative.Env Expression → Prop} (h : Triple π params Pre ss Post factory) (hpost_proj : Imperative.Logic.Hoare.PostWF ss Post) : Triple π params Pre [Imperative.Stmt.block l ss md] Post factory

Wrap a statement list in a labelled block. Post must not mention the names the body scopes (PostWF); no statement step mutates the factory across the body, so leaving the block restores nothing.

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

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) {factory : Lambda.Factory CoreLParams} (params : InitEnvWFParams) {cond : Expression.Expr} {tss ess : Statements} {md : Imperative.MetaData Expression} {Pre Post : Imperative.Env Expression → Prop} (ht : Triple π params (fun (ρ : Imperative.Env Expression) => Pre ρ ∧ Expression.eval ρ.factory ρ.store cond = some (Imperative.HasBool.ttVal ρ.factory)) tss Post factory) (he : Triple π params (fun (ρ : Imperative.Env Expression) => Pre ρ ∧ Expression.eval ρ.factory ρ.store cond = some (Imperative.HasBool.ffVal ρ.factory)) ess Post factory) (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 factory

If-then-else rule.

theorem Core.Logic.Hoare.while_rule (π : String → Option Procedure) {factory : Lambda.Factory CoreLParams} (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} (hbody : Triple π params (fun (ρ : Imperative.Env Expression) => Inv ρ ∧ Expression.eval ρ.factory ρ.store guard = some (Imperative.HasBool.ttVal ρ.factory)) body Inv factory) (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.ffVal ρ.factory)) factory

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.