Semantic well-formedness of captured events

Each event captures the factory and store at the moment it is emitted. EventArg.SemanticWF records that the captured store holds only values and that the captured factory's evaluator respects free-variable store agreement. Event.semanticWF and Trace.semanticWF lift it to events and traces.

These definitions depend on the evaluator conditions in Strata.DL.Imperative.CmdSemantics, which itself imports Strata.DL.Imperative.CmdTrace, so they live here rather than beside EventArg.

structure Imperative.EventArg.SemanticWF {P : PureExpr} [HasVal P] [HasFvars P] (arg : EventArg P) : Prop

Semantic evidence carried by an event-argument snapshot.

• storeWellDefined : WellFormedStore arg.store arg.factory
• exprCongr : WellFormedSemanticEvalExprCongr arg.factory

def Imperative.Event.semanticWF {P : PureExpr} [HasVal P] [HasFvars P] : Event P → Prop

Semantic evidence carried by an event snapshot.

Equations

• (Imperative.Event.assert arg).semanticWF = arg.SemanticWF
• (Imperative.Event.assume arg).semanticWF = arg.SemanticWF
• (Imperative.Event.cover arg).semanticWF = arg.SemanticWF

def Imperative.Trace.semanticWF {P : PureExpr} [HasVal P] [HasFvars P] (trace : Trace P) : Prop

Every event snapshot in a trace is semantically well formed.

Equations

• trace.semanticWF = ∀ (event : Imperative.Event P), event ∈ trace → event.semanticWF

theorem Imperative.Trace.semanticWF_append {P : PureExpr} [HasVal P] [HasFvars P] {first second : Trace P} (hfirst : first.semanticWF) (hsecond : second.semanticWF) : (first ++ second).semanticWF

Semantic snapshot evidence composes across trace concatenation.