Core-specific residue of the call-free bridge

The generic call-free bridge between extended (CmdExt P) and base (Cmd P) Imperative syntax, and all of its command-generic properties, live in Strata.DL.Imperative.StmtExtendCallBridge(Props). Core specializes that bridge at its expression type Expression (so CmdExt Expression = Command) simply by using the generic embed* / project* API.

This module keeps only what is genuinely Core-specific — the facts that mention a concrete call predicate or Core's init-environment well-formedness, and cannot be stated at the generic layer:

• projection succeeds exactly on the call-free fragment, phrased with Core's Statement.isNotCall / Statements.noCalls; and
• Core BlockInitEnvWF transports across projection and embedding (Core.Logic), phrased with InitEnvWFParams and both the Core and generic BlockInitEnvWF; and
• through the embedding, the runs of a call-free Core statement list are runs over base commands, so every event they emit is captured under the entry's factory (Core.Logic.coreBlock_events_factory, coreBlock_terminatesAt_events_factory) and a completed run keeps the entry's factory and its defined bindings (Core.Logic.coreBlock_terminatesAt_env).

Everything else (inversion, round trips, injectivity, analysis commutation, and the native event-step/star correspondence) is reused from the generic module.

Projection succeeds exactly on the call-free fragment

These are the only bridge facts that mention Core's concrete call predicates Statement.isNotCall / Statements.noCalls, so they stay Core-side.

theorem Core.projectStmt_some_of_allSubstmts {s : Statement} (h : Imperative.Stmt.allSubstmts Statement.isNotCall s = true) : ∃ (b : Imperative.Stmt Expression (Imperative.Cmd Expression)), Imperative.projectStmt s = some b

A Core statement all of whose substatements are non-calls projects successfully to a base statement.

theorem Core.projectStmts_some_of_allSubstmts {ss : Statements} (h : Imperative.Block.allSubstmts Statement.isNotCall ss = true) : ∃ (bs : List (Imperative.Stmt Expression (Imperative.Cmd Expression))), Imperative.projectStmts ss = some bs

A Core statement list all of whose substatements are non-calls projects successfully to base statements.

theorem Core.noCalls_projectStmts {ss : Statements} (h : ss.noCalls = true) : ∃ (bs : List (Imperative.Stmt Expression (Imperative.Cmd Expression))), Imperative.projectStmts ss = some bs ∧ Imperative.embedStmts bs = ss

A call-free list of Core statements is the embedding of its projection: projection succeeds and re-embeds to the original.

The embedding lands in the call-free fragment

theorem Core.embedStmt_allSubstmts_isNotCall (s : Imperative.Stmt Expression (Imperative.Cmd Expression)) : Imperative.Stmt.allSubstmts Statement.isNotCall (Imperative.embedStmt s) = true

Every substatement of an embedded base statement is a non-call.

theorem Core.embedStmts_allSubstmts_isNotCall (ss : List (Imperative.Stmt Expression (Imperative.Cmd Expression))) : Imperative.Block.allSubstmts Statement.isNotCall (Imperative.embedStmts ss) = true

Every substatement of an embedded base statement list is a non-call.

theorem Core.noCalls_embedStmts (ss : List (Imperative.Stmt Expression (Imperative.Cmd Expression))) : Statements.noCalls (Imperative.embedStmts ss) = true

The embedding of any base block is call-free.

theorem Core.noCalls_of_projectStmts_ok {ss : Statements} {bs : List (Imperative.Stmt Expression (Imperative.Cmd Expression))} (h : Imperative.projectStmts ss = some bs) : ss.noCalls = true

A Core block that projects successfully is call-free: projection succeeds exactly on the call-free fragment.

theorem Core.Logic.BlockInitEnvWF.ofBaseEmbed {params : InitEnvWFParams} {bs : List (Imperative.Stmt Expression (Imperative.Cmd Expression))} {ρ : Imperative.Env Expression} (hwf : Imperative.WellFormedSemanticEval ρ.factory) (hsv : Imperative.WellFormedStore ρ.store ρ.factory) (hdefs : ∀ (n : Expression.Ident), n ∈ Imperative.Block.definedVars bs false → (ρ.store n).isNone = true) (hdnr : ∀ (n : Expression.Ident), n ∈ Imperative.Block.definedVars bs false → ∀ (p : String), p ∈ params.prefixIdents → ¬p.toList.isPrefixOf n.name.toList = true) (hres : ∀ (n : Expression.Ident), (ρ.store n).isSome = true → ∀ (p : String), p ∈ params.prefixIdents → ¬p.toList.isPrefixOf n.name.toList = true) (hlab : ∀ (l : String), l ∈ Imperative.Block.labels bs → ∀ (p : String), p ∈ params.prefixBlockLabels → ¬p.toList.isPrefixOf l.toList = true) (hdu : Imperative.Block.defUseWellFormed (fun (n : Expression.Ident) => (ρ.store n).isSome) params.declaredFuncs bs = true) (hfd : ∀ (nm : String), isNameInFactory nm = true → params.declaredFuncs { name := nm, metadata := () } = true) (hinit : Imperative.Block.InitTypesInhabited ρ.factory bs) (hty : ∃ (Γ : Imperative.VarTyping Expression), Imperative.StoreHasTyping ρ.factory ρ.store Γ ∧ Imperative.Block.fvarTypesWellAnnotated Γ bs) (hmt : ∀ (m : Expression.Expr), m ∈ Imperative.Block.measures bs → Expression.HasType (Expression.annotationTyping m) m Imperative.HasInt.intTy) : BlockInitEnvWF params (Imperative.embedStmts bs) ρ

Output transport. Re-establish the full Core BlockInitEnvWF on an embedded base block embedStmts bs from the corresponding base conditions stated over bs.

The statement-independent fields (evaluator well-formedness, store well-definedness, reserved-prefix freshness, factory-declaredness) are passed through verbatim; the block-shaped fields (defsUndefined, definedVarsNotReserved, exitsNotReserved, defUseOk, initTypesInhabited, fvarTypesOk, measuresTyped, and the readWritesDefined it subsumes) are discharged by rewriting each Core analysis on embedStmts bs to the corresponding base analysis on bs.

theorem Core.Logic.BlockInitEnvWF.toImperativeProject {params : InitEnvWFParams} {ss : Statements} {bs : List (Imperative.Stmt Expression (Imperative.Cmd Expression))} {ρ : Imperative.Env Expression} (h : BlockInitEnvWF params ss ρ) (hp : Imperative.projectStmts ss = some bs) : Imperative.Logic.BlockInitEnvWF params bs ρ

Input transport (to the generic gate). A Core BlockInitEnvWF on ss weakens to the generic Imperative.Logic.BlockInitEnvWF on the base block bs that ss projects to, with the same params. This is the bridged analogue of BlockInitEnvWF.toImperative, exposing the generic base-language gate for the projected block.

theorem Core.Logic.blockInitEnvWF_projectBase {params : InitEnvWFParams} {ss : Statements} {bs : List (Imperative.Stmt Expression (Imperative.Cmd Expression))} {ρ : Imperative.Env Expression} (h : BlockInitEnvWF params ss ρ) (hp : Imperative.projectStmts ss = some bs) : Imperative.WellFormedSemanticEval ρ.factory ∧ Imperative.WellFormedStore ρ.store ρ.factory ∧ (∀ (n : Expression.Ident), n ∈ Imperative.Block.definedVars bs false → (ρ.store n).isNone = true) ∧ (∀ (n : Expression.Ident), n ∈ Imperative.Block.definedVars bs false → ∀ (p : String), p ∈ params.prefixIdents → ¬p.toList.isPrefixOf n.name.toList = true) ∧ (∀ (n : Expression.Ident), (ρ.store n).isSome = true → ∀ (p : String), p ∈ params.prefixIdents → ¬p.toList.isPrefixOf n.name.toList = true) ∧ (∀ (l : String), l ∈ Imperative.Block.labels bs → ∀ (p : String), p ∈ params.prefixBlockLabels → ¬p.toList.isPrefixOf l.toList = true) ∧ Imperative.Block.defUseWellFormed (fun (n : Expression.Ident) => (ρ.store n).isSome) params.declaredFuncs bs = true ∧ (∀ (nm : String), isNameInFactory nm = true → params.declaredFuncs { name := nm, metadata := () } = true) ∧ Imperative.Block.InitTypesInhabited ρ.factory bs ∧ (∃ (Γ : Imperative.VarTyping Expression), Imperative.StoreHasTyping ρ.factory ρ.store Γ ∧ Imperative.Block.fvarTypesWellAnnotated Γ bs) ∧ ∀ (m : Expression.Expr), m ∈ Imperative.Block.measures bs → Expression.HasType (Expression.annotationTyping m) m Imperative.HasInt.intTy

Extract every Core initial-environment condition for the projected base block bs.

theorem Core.Logic.blockInitEnvWF_project_embed {params : InitEnvWFParams} {ss : Statements} {bs : List (Imperative.Stmt Expression (Imperative.Cmd Expression))} {ρ : Imperative.Env Expression} (h : BlockInitEnvWF params ss ρ) (hp : Imperative.projectStmts ss = some bs) : BlockInitEnvWF params (Imperative.embedStmts bs) ρ

Projecting a call-free Core block to base statements and re-embedding it preserves BlockInitEnvWF.

Runs of call-free statement lists

theorem Core.Logic.coreBlock_events_factory {π : String → Option Procedure} {ss : Statements} {ρ₀ : Imperative.Env Expression} {trace : Imperative.Trace Expression} {cfg : Imperative.Config Expression Command} (hnc : ss.noCalls = true) (h : (EventLang.coreBlock π).traceStar ((EventLang.coreBlock π).stmtCfg ss ρ₀) trace cfg) (ev : Imperative.Event Expression) : ev ∈ trace → ev.condition.factory = ρ₀.factory

Every event of a call-free Core run is captured under the entry's factory. For a call-free Core statement list ss, every event of every trace of ss from ρ₀ has the factory of ρ₀.

theorem Core.Logic.coreBlock_terminatesAt_events_factory {π : String → Option Procedure} {ss : Statements} {ρ₀ ρ' : Imperative.Env Expression} {trace : Imperative.Trace Expression} (hnc : ss.noCalls = true) (h : (EventLang.coreBlock π).TerminatesAt ss ρ₀ trace ρ') (ev : Imperative.Event Expression) : ev ∈ trace → ev.condition.factory = ρ₀.factory

Every event of a completed call-free Core run is captured under the entry's factory. For a call-free Core statement list ss and a run of ss from ρ₀ ending normally or by an exit, every event of its trace has the factory of ρ₀.

theorem Core.Logic.coreBlock_terminatesAt_env {π : String → Option Procedure} {ss : Statements} {ρ₀ ρ' : Imperative.Env Expression} {trace : Imperative.Trace Expression} (hnc : ss.noCalls = true) (h : (EventLang.coreBlock π).TerminatesAt ss ρ₀ trace ρ') : ρ'.factory = ρ₀.factory ∧ ∀ (x : Expression.Ident), (ρ₀.store x).isSome = true → (ρ'.store x).isSome = true

A completed call-free Core run keeps the entry's factory and its bindings. For a call-free Core statement list ss and a run of ss from ρ₀ ending normally or by an exit in ρ': ρ' has the factory of ρ₀, and every variable defined in ρ₀ is defined in ρ'.