Properties of the Imperative trace relations

Companion to Strata.DL.Imperative.Logic.TraceRelations, which carries the compact definitions of the trace relations Trace.StuttersEnv / TraceExtendsEnv; the event-level relations they build on, EventArg.ExtendsEnv / Event.ExtendsEnv, are defined in Strata.DL.Imperative.CmdTrace. This module collects the property proofs for all four. The store- and environment-level laws live with the semantics they belong to: the command-level StoreAgreement and StoreExtendsWith laws in Strata.DL.Imperative.StoreRelationsProps, and the statement-level StoreExtendsWith.projectStore, StoreAgreement.of_projectStore, and Env.ExtendsWith.refl / .trans_union in Strata.DL.Imperative.StmtSemanticsProps.

Key theorem families:

• evalCmdE_replay_extends replays a canonical event-producing command on an extending target store, preserving the classified store extension and relating the emitted snapshots by the pointwise TraceExtendsEnv.
• Composition laws EventArg.ExtendsEnv.trans_union / Event.ExtendsEnv.trans_union / TraceExtendsEnv.trans_union chain two stages while unioning their extra-register classes.
• Semantic transport laws transfer assumption satisfaction and reachability forward across Trace.StuttersEnv, and reflect assertion validity backward, under ConditionInterp.StableUnderExtendsEnv and ConditionInterp.TrueStutterHolds.
• Reflexivity / monotonicity / append laws for each relation, the Trace.StuttersEnv.Cmd.emittedEvents_stuttersEnv command-snapshot law, and the TraceExtendsEnv.toTraceStuttersEnv refinement.
• Semantic matching TraceExtendsEnv.toMatches upgrades lockstep extension to a pointwise match under any semantic argument relation, given defined source reads and well-formed snapshots; Event.Matches.comp and Trace.matches_comp compose such matches.
• WithWF strengthenings of EventArg.ExtendsEnv (EventArg.WithWF is defined in TraceRelations): EventArg.WithWF.mono / trans / label_metadata / factory_label_metadata, with trace-level Trace.WithWF.append / toExtendsEnv / of_extends / mono / trans / toTraceStuttersEnv / assertionValidFrom_reflect.
• Trace.WeakensAssumes is reflexive and transitive (Trace.WeakensAssumes.refl, Trace.WeakensAssumes.trans), as is its event-level counterpart relation Event.WeakensAssume. It carries assumption satisfaction from the source to the target (Trace.WeakensAssumes.assumptionsHold_transfer) and reflects assertion validity from the target to the source (Trace.WeakensAssumes.assertionsValid_reflect).
• Trace.InsertsTrueAssumes is reflexive and closed under concatenation (refl, append) and carries assumption satisfaction forward under ConditionInterp.TrueStutterHolds (assumptionsHold). So is its composition with Trace.MayDropEvents, a List.Sublist (Trace.mayDropEvents_insertsTrueAssumes_*; drop_left drops a prefix of the source). Trace.PreservesLastEvent composes on the left (append_left), and a relation preserving the last event followed by extra events reflects last assertions (Trace.PreservesLastEvent.reflectsLastAssertion).
• Trace.InsertsAsserts and Trace.InsertsCheckedAssumes hold under a larger set of allowed factories (mono_allowed), and, under an interpretation for which conditions with the same value hold alike (and, for the second, true conditions hold), reflect assertion validity (reflect, assertionsValidFromP_reflect) and carry reachability forward (reachable_transfer, for the second when the inserted checks of the target are valid); so does their composition (Trace.insertsAsserts_insertsCheckedAssumes_*).

theorem Imperative.EventArg.ExtendsEnv.eq_of_false {P : PureExpr} {source target : EventArg P} (h : ExtendsEnv (fun (x : P.Ident) => False) source target) : source = target

With no permitted target-only bindings, event-argument extension is ordinary equality.

theorem Imperative.EventArg.ExtendsEnv.refl {P : PureExpr} (Extra : P.Ident → Prop) (arg : EventArg P) : ExtendsEnv Extra arg arg

Every event argument extends itself.

theorem Imperative.EventArg.ExtendsEnv.mono {P : PureExpr} {Extra Extra' : P.Ident → Prop} (hsub : ∀ (ident : P.Ident), Extra ident → Extra' ident) {source target : EventArg P} (h : ExtendsEnv Extra source target) : ExtendsEnv Extra' source target

Widening the accepted class of target-only registers preserves event-argument extension.

theorem Imperative.EventArg.ExtendsEnv.trans_union {P : PureExpr} {Extra₁ Extra₂ : P.Ident → Prop} {first second third : EventArg P} (h₁ : ExtendsEnv Extra₁ first second) (h₂ : ExtendsEnv Extra₂ second third) : ExtendsEnv (fun (ident : P.Ident) => Extra₁ ident ∨ Extra₂ ident) first third

Event-argument extension composes while unioning extra-register classes.

theorem Imperative.ConditionInterp.stableUnderExtendsEnv_false {P : PureExpr} (I : ConditionInterp P) : I.StableUnderExtendsEnv fun (x : P.Ident) => False

Every condition interpretation is stable when target-only bindings are forbidden: EventArg.ExtendsEnv false is equality, so both interpreted conditions are identical.

theorem Imperative.Event.ExtendsEnv.refl {P : PureExpr} (Extra : P.Ident → Prop) (event : Event P) : ExtendsEnv Extra event event

Every event extends itself.

theorem Imperative.Event.ExtendsEnv.mono {P : PureExpr} {Extra Extra' : P.Ident → Prop} (hsub : ∀ (ident : P.Ident), Extra ident → Extra' ident) {source target : Event P} (h : ExtendsEnv Extra source target) : ExtendsEnv Extra' source target

Widening the accepted class of target-only registers preserves event extension.

theorem Imperative.Event.ExtendsEnv.trans_union {P : PureExpr} {Extra₁ Extra₂ : P.Ident → Prop} {first second third : Event P} (h₁ : ExtendsEnv Extra₁ first second) (h₂ : ExtendsEnv Extra₂ second third) : ExtendsEnv (fun (ident : P.Ident) => Extra₁ ident ∨ Extra₂ ident) first third

Event extension composes while unioning extra-register classes.

theorem Imperative.Trace.StuttersEnv.refl {P : PureExpr} [HasBool P] (allowedVarName : P.Ident → Prop) (allowedFactory : P.Factory → Prop) (trace : Trace P) : StuttersEnv allowedVarName allowedFactory trace trace

Every trace extends itself.

theorem Imperative.Trace.StuttersEnv.mono {P : PureExpr} [HasBool P] {allowedVarName allowedVarName' : P.Ident → Prop} {allowedFactory : P.Factory → Prop} (hsub : ∀ (ident : P.Ident), allowedVarName ident → allowedVarName' ident) {source target : Trace P} (h : StuttersEnv allowedVarName allowedFactory source target) : StuttersEnv allowedVarName' allowedFactory source target

Widening the accepted class of target-only registers preserves environment-extending trace correspondence.

theorem Imperative.Trace.StuttersEnv.append {P : PureExpr} [HasBool P] {allowedVarName : P.Ident → Prop} {allowedFactory : P.Factory → Prop} {source₁ target₁ source₂ target₂ : Trace P} (h₁ : StuttersEnv allowedVarName allowedFactory source₁ target₁) (h₂ : StuttersEnv allowedVarName allowedFactory source₂ target₂) : StuttersEnv allowedVarName allowedFactory (source₁ ++ source₂) (target₁ ++ target₂)

Environment-extending trace correspondence composes over chronological append.

theorem Imperative.Trace.StuttersEnv.prepend {P : PureExpr} [HasBool P] (allowedVarName : P.Ident → Prop) (allowedFactory : P.Factory → Prop) (common : Trace P) {source target : Trace P} (h : StuttersEnv allowedVarName allowedFactory source target) : StuttersEnv allowedVarName allowedFactory (common ++ source) (common ++ target)

A common exact prefix preserves environment-extending trace correspondence.

Semantic transport across Trace.StuttersEnv

theorem Imperative.Trace.StuttersEnv.assumptionsHold_transfer {P : PureExpr} [HasBool P] {I : ConditionInterp P} {allowedVarName : P.Ident → Prop} {allowedFactory : P.Factory → Prop} (hstable : I.StableUnderExtendsEnv allowedVarName) (htrue : I.TrueStutterHolds allowedFactory) {source target : Trace P} (h : StuttersEnv allowedVarName allowedFactory source target) (world : I.World) : AssumptionsHold P I world source → AssumptionsHold P I world target

Trace.StuttersEnv transfers assumption satisfaction from source to target: any world satisfying the source trace's assumptions satisfies the target's. Dropped-left stutter weakens the source assumptions; inserted-right stutter adds an assumption the evaluator deemed true (htrue); and paired assumptions agree by stability (hstable).

theorem Imperative.Trace.StuttersEnv.reachable_transfer {P : PureExpr} [HasBool P] {I : ConditionInterp P} {allowedVarName : P.Ident → Prop} {allowedFactory : P.Factory → Prop} (hstable : I.StableUnderExtendsEnv allowedVarName) (htrue : I.TrueStutterHolds allowedFactory) {source target : Trace P} (h : StuttersEnv allowedVarName allowedFactory source target) (hreach : Reachable P I source) : Reachable P I target

Trace.StuttersEnv transfers reachability forward: a reachable source trace has a reachable target trace (same world witness).

theorem Imperative.Trace.StuttersEnv.assertionsValid_reflect {P : PureExpr} [HasBool P] {I : ConditionInterp P} {allowedVarName : P.Ident → Prop} {allowedFactory : P.Factory → Prop} (hstable : I.StableUnderExtendsEnv allowedVarName) (htrue : I.TrueStutterHolds allowedFactory) {source target : Trace P} (h : StuttersEnv allowedVarName allowedFactory source target) (hvalid : AssertionsValid P I target) : AssertionsValid P I source

Whole-trace validity reflection across Trace.StuttersEnv: target validity reflects to source validity under semantic stability. The empty-accumulator instance of assertionsValidFrom_reflect.

theorem Imperative.TraceExtendsEnv.refl {P : PureExpr} (allowedVarName : P.Ident → Prop) (trace : Trace P) : TraceExtendsEnv allowedVarName trace trace

Every trace is in lockstep with itself.

theorem Imperative.TraceExtendsEnv.mono {P : PureExpr} {allowedVarName allowedVarName' : P.Ident → Prop} (hsub : ∀ (ident : P.Ident), allowedVarName ident → allowedVarName' ident) {source target : Trace P} (h : TraceExtendsEnv allowedVarName source target) : TraceExtendsEnv allowedVarName' source target

Widening the accepted class of target-only registers preserves lockstep trace correspondence.

theorem Imperative.TraceExtendsEnv.append {P : PureExpr} {allowedVarName : P.Ident → Prop} {source₁ target₁ source₂ target₂ : Trace P} (h₁ : TraceExtendsEnv allowedVarName source₁ target₁) (h₂ : TraceExtendsEnv allowedVarName source₂ target₂) : TraceExtendsEnv allowedVarName (source₁ ++ source₂) (target₁ ++ target₂)

Lockstep trace correspondence composes over chronological append.

theorem Imperative.TraceExtendsEnv.Cmd.emittedEvents_extendsEnv {P : PureExpr} [HasBool P] (allowedVarName : P.Ident → Prop) (command : Cmd P) (factory : P.Factory) {sourceStore targetStore : SemanticStore P} (hstore : StoreExtendsWith allowedVarName sourceStore targetStore) : TraceExtendsEnv allowedVarName (Cmd.emittedEvents P command factory sourceStore) (Cmd.emittedEvents P command factory targetStore)

The same command observed in classified extending stores emits lockstep-related traces. Each command emits a fixed number of events whose kind depends only on the command, not on the store, so the source and target traces have equal length and their single (assert/assume/cover) event corresponds by Event.ExtendsEnv.

theorem Imperative.TraceExtendsEnv.trans_union {P : PureExpr} {allowedVarName₁ allowedVarName₂ : P.Ident → Prop} {source middle target : Trace P} (h₁ : TraceExtendsEnv allowedVarName₁ source middle) (h₂ : TraceExtendsEnv allowedVarName₂ middle target) : TraceExtendsEnv (fun (ident : P.Ident) => allowedVarName₁ ident ∨ allowedVarName₂ ident) source target

Consecutive lockstep correspondences compose, unioning the accepted target-only register classes. This is the sound transitivity principle Trace.StuttersEnv lacks: two-sided true-event stuttering would let a middle event be extended to one reading a newly added binding, but a lockstep middle event is matched exactly, so the classes compose.

theorem Imperative.TraceExtendsEnv.trans {P : PureExpr} {allowedVarName : P.Ident → Prop} {source middle target : Trace P} (h₁ : TraceExtendsEnv allowedVarName source middle) (h₂ : TraceExtendsEnv allowedVarName middle target) : TraceExtendsEnv allowedVarName source target

Consecutive lockstep correspondences using the same accepted class compose.

theorem Imperative.TraceExtendsEnv.toTraceStuttersEnv {P : PureExpr} [HasBool P] {allowedVarName : P.Ident → Prop} {allowedFactory : P.Factory → Prop} {source target : Trace P} (h : TraceExtendsEnv allowedVarName source target) : Trace.StuttersEnv allowedVarName allowedFactory source target

Pointwise trace correspondence refines the stuttering correspondence: every pointwise (lockstep) step is in particular a non-stuttering Trace.StuttersEnv step.

theorem Imperative.Trace.StuttersEnv.Cmd.emittedEvents_stuttersEnv {P : PureExpr} [HasBool P] (allowedVarName : P.Ident → Prop) (allowedFactory : P.Factory → Prop) (command : Cmd P) (factory : P.Factory) {sourceStore targetStore : SemanticStore P} (hstore : StoreExtendsWith allowedVarName sourceStore targetStore) : StuttersEnv allowedVarName allowedFactory (Cmd.emittedEvents P command factory sourceStore) (Cmd.emittedEvents P command factory targetStore)

The same command observed in classified extending stores emits stutter-related traces, as a corollary of its pointwise event correspondence.

theorem Imperative.evalCmdE_replay_extends {P : PureExpr} [HasFvar P] [HasFvars P] [HasBoolOps P] [HasIdent P] [DecidableEq P.Ident] (Extra : P.Ident → Prop) (f : P.Factory) (σs σt σs' : SemanticStore P) (c : Cmd P) (emitted : Trace P) (hext : StoreExtendsWith Extra σs σt) (heval : EvalCmdE P f σs c σs' emitted) (hwf : WellFormedSemanticEvalMono f) (hinit : ∀ (x : P.Ident), x ∈ c.definedVars → σt x = none) : ∃ (σt' : SemanticStore P), EvalCmdE P f σt c σt' (Cmd.emittedEvents P c f σt) ∧ StoreExtendsWith Extra σs' σt' ∧ TraceExtendsEnv Extra emitted (Cmd.emittedEvents P c f σt)

Replay a canonical event-producing command on an extending target store, in pointwise lockstep. The replay preserves classified store extension and relates the command's observable snapshots with the pointwise TraceExtendsEnv.

Key idea: replaying the same command c on an extending store emits the same number and kinds of events because event shape depends only on the command, so the source and target traces correspond event-by-event. Store extension supplies every value read by the source evaluation and is preserved by the resulting store updates.

theorem Imperative.TraceExtendsEnv.toMatches {P : PureExpr} [HasVal P] [HasFvars P] {Extra : P.Ident → Prop} {ArgRel : EventArg P → EventArg P → Prop} (hmk : ∀ {source target : EventArg P}, EventArg.ExtendsEnv Extra source target → StoreAgreesOnFvars source.store target.store source.expr → source.SemanticWF → target.SemanticWF → ArgRel source target) {source target : Trace P} (hext : TraceExtendsEnv Extra source target) (hreads : source.readsDefined) (hsourceWF : source.semanticWF) (htargetWF : target.semanticWF) : List.Rel₂ (Event.Matches ArgRel) source target

Pointwise environment extension strengthens to any semantic argument relation once source reads are defined and both traces carry well-formed snapshots. Source-defined free variables are preserved by the store extension, which supplies free-variable store agreement.

theorem Imperative.Event.Matches.comp {P : PureExpr} {R₁ R₂ R₃ : EventArg P → EventArg P → Prop} (hcomp : ∀ {first second third : EventArg P}, R₁ first second → R₂ second third → R₃ first third) {first second third : Event P} (h₁ : Matches R₁ first second) (h₂ : Matches R₂ second third) : Matches R₃ first third

Same-kind event matching composes through a middle event.

theorem Imperative.Trace.matches_comp {P : PureExpr} {R₁ R₂ R₃ : EventArg P → EventArg P → Prop} (hcomp : ∀ {first second third : EventArg P}, R₁ first second → R₂ second third → R₃ first third) {first second third : Trace P} (h₁ : List.Rel₂ (Event.Matches R₁) first second) (h₂ : List.Rel₂ (Event.Matches R₂) second third) : List.Rel₂ (Event.Matches R₃) first third

Pointwise same-kind event matching composes through a middle trace.

WithWF strengthenings of ExtendsEnv

theorem Imperative.EventArg.WithWF.mono {P : PureExpr} [HasVal P] [HasFvars P] {Extra Extra' : P.Ident → Prop} (hsub : ∀ (ident : P.Ident), Extra ident → Extra' ident) {source target : EventArg P} (h : WithWF (ExtendsEnv Extra) source target) : WithWF (ExtendsEnv Extra') source target

Widening the accepted class of target-only bindings preserves WithWF (ExtendsEnv _).

theorem Imperative.EventArg.WithWF.trans {P : PureExpr} [HasVal P] [HasFvars P] {Extra₁ Extra₂ : P.Ident → Prop} {first second third : EventArg P} (h₁ : WithWF (ExtendsEnv Extra₁) first second) (h₂ : WithWF (ExtendsEnv Extra₂) second third) : WithWF (ExtendsEnv fun (ident : P.Ident) => Extra₁ ident ∨ Extra₂ ident) first third

WithWF (ExtendsEnv _) composes while unioning the classes of target-only bindings.

theorem Imperative.EventArg.WithWF.label_metadata {P : PureExpr} [HasVal P] [HasFvars P] {Extra : P.Ident → Prop} {source target : EventArg P} (h : WithWF (ExtendsEnv Extra) source target) : source.label = target.label ∧ source.metadata = target.metadata

Arguments related by WithWF (ExtendsEnv _) carry the same assertion label and metadata.

theorem Imperative.EventArg.WithWF.factory_label_metadata {P : PureExpr} [HasVal P] [HasFvars P] {Extra : P.Ident → Prop} {source target : EventArg P} (h : WithWF (ExtendsEnv Extra) source target) : target.factory = source.factory ∧ source.label = target.label ∧ source.metadata = target.metadata

WithWF (ExtendsEnv _) keeps the factory, the label and the metadata of the source argument.

theorem Imperative.Event.WithWF.toExtendsEnv {P : PureExpr} [HasVal P] [HasFvars P] {Extra : P.Ident → Prop} {source target : Event P} (h : WithWF (EventArg.ExtendsEnv Extra) source target) : ExtendsEnv Extra source target

Forgetting the well-formedness evidence recovers ordinary event extension.

theorem Imperative.Trace.WithWF.append {P : PureExpr} [HasVal P] [HasFvars P] {R : EventArg P → EventArg P → Prop} {s₁ s₂ t₁ t₂ : Trace P} (h₁ : WithWF R s₁ t₁) (h₂ : WithWF R s₂ t₂) : WithWF R (s₁ ++ s₂) (t₁ ++ t₂)

Trace.WithWF R is closed under append, for any argument relation R.

theorem Imperative.Trace.WithWF.toExtendsEnv {P : PureExpr} [HasVal P] [HasFvars P] {Extra : P.Ident → Prop} {source target : Trace P} (h : WithWF (EventArg.ExtendsEnv Extra) source target) : TraceExtendsEnv Extra source target

Forgetting the well-formedness evidence pointwise recovers trace extension.

theorem Imperative.Trace.WithWF.of_extends {P : PureExpr} [HasVal P] [HasFvars P] {Extra : P.Ident → Prop} {source target : Trace P} (hext : TraceExtendsEnv Extra source target) (hreads : source.readsDefined) (hsourceWF : source.semanticWF) (htargetWF : target.semanticWF) : WithWF (EventArg.ExtendsEnv Extra) source target

Ordinary lockstep extension strengthens to WithWF matching when source event reads are defined and both traces carry well-formed snapshots.

theorem Imperative.Trace.WithWF.mono {P : PureExpr} [HasVal P] [HasFvars P] {Extra Extra' : P.Ident → Prop} (hsub : ∀ (ident : P.Ident), Extra ident → Extra' ident) {source target : Trace P} (h : WithWF (EventArg.ExtendsEnv Extra) source target) : WithWF (EventArg.ExtendsEnv Extra') source target

Widening the accepted class of target-only bindings preserves Trace.WithWF (ExtendsEnv _).

theorem Imperative.Trace.WithWF.trans {P : PureExpr} [HasVal P] [HasFvars P] {Extra₁ Extra₂ : P.Ident → Prop} {first second third : Trace P} (h₁ : WithWF (EventArg.ExtendsEnv Extra₁) first second) (h₂ : WithWF (EventArg.ExtendsEnv Extra₂) second third) : WithWF (EventArg.ExtendsEnv fun (ident : P.Ident) => Extra₁ ident ∨ Extra₂ ident) first third

Trace.WithWF (ExtendsEnv _) composes through a middle trace while unioning the classes of target-only bindings.

theorem Imperative.Trace.WithWF.toTraceStuttersEnv {P : PureExpr} [HasBool P] [HasFvars P] {Extra : P.Ident → Prop} {allowedFactory : P.Factory → Prop} {source target : Trace P} (h : WithWF (EventArg.ExtendsEnv Extra) source target) : StuttersEnv Extra allowedFactory source target

Trace.WithWF (ExtendsEnv _) is also a stuttering correspondence.

theorem Imperative.Trace.WithWF.assertionValidFrom_reflect {P : PureExpr} [HasVal P] [HasFvars P] {Extra : P.Ident → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.WithWF (EventArg.ExtendsEnv Extra))) {source target : Trace P} (h : WithWF (EventArg.ExtendsEnv Extra) source target) (aid : AssertId P) : AssertionValidFrom P I aid [] target → AssertionValidFrom P I aid [] source

Trace.WithWF (ExtendsEnv _) reflects assertion validity for any condition interpretation stable under EventArg.WithWF (ExtendsEnv _).

theorem Imperative.Event.WeakensAssume.refl {P : PureExpr} (I : ConditionInterp P) (e : Event P) : WeakensAssume I e e

Every event is its own counterpart.

theorem Imperative.Event.WeakensAssume.trans {P : PureExpr} {I : ConditionInterp P} {e₁ e₂ e₃ : Event P} (h₁ : WeakensAssume I e₁ e₂) (h₂ : WeakensAssume I e₂ e₃) : WeakensAssume I e₁ e₃

Counterparts compose.

theorem Imperative.Trace.WeakensAssumes.refl {P : PureExpr} (I : ConditionInterp P) (t : Trace P) : WeakensAssumes I t t

Trace.WeakensAssumes I is reflexive.

theorem Imperative.Trace.WeakensAssumes.trans {P : PureExpr} {I : ConditionInterp P} {t₁ t₂ t₃ : Trace P} (h₁ : WeakensAssumes I t₁ t₂) (h₂ : WeakensAssumes I t₂ t₃) : WeakensAssumes I t₁ t₃

Trace.WeakensAssumes I is transitive: an event of the middle trace that is dropped from the last one is an assumption, so its counterpart in the first trace is one too and is dropped.

theorem Imperative.Trace.WeakensAssumes.assumptionsHold_transfer {P : PureExpr} {I : ConditionInterp P} {s t : Trace P} (h : WeakensAssumes I s t) {w : I.World} (hs : AssumptionsHold P I w s) : AssumptionsHold P I w t

Assumptions of the source holding in a world hold in it for the target: every assumption of the target is the counterpart of one of the source, which holds in every world the source's does.

theorem Imperative.Trace.WeakensAssumes.assertionsValid_reflect {P : PureExpr} {I : ConditionInterp P} {s t : Trace P} (h : WeakensAssumes I s t) (hv : AssertionsValid P I t) : AssertionsValid P I s

Assertion validity reflects from the target to the source.

theorem Imperative.Trace.InsertsTrueAssumes.refl {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} (t : Trace P) : InsertsTrueAssumes allowed t t

Every trace is itself with no assumption inserted.

theorem Imperative.Trace.InsertsTrueAssumes.append {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {a a' b b' : Trace P} (ha : InsertsTrueAssumes allowed a a') (hb : InsertsTrueAssumes allowed b b') : InsertsTrueAssumes allowed (a ++ b) (a' ++ b')

Trace.InsertsTrueAssumes is closed under concatenation.

theorem Imperative.Trace.InsertsTrueAssumes.assumptionsHold {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {I : ConditionInterp P} (htrue : I.TrueStutterHolds allowed) {t t' : Trace P} (h : InsertsTrueAssumes allowed t t') {w : I.World} (hA : AssumptionsHold P I w t) : AssumptionsHold P I w t'

The assumptions of t with true assumptions inserted hold in every world where those of t hold, when every operationally true condition under an allowed factory holds in every world.

theorem Imperative.Trace.mayDropEvents_insertsTrueAssumes_refl {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} (t : Trace P) : RComp MayDropEvents (InsertsTrueAssumes allowed) t t

Dropping events, then inserting true assumptions, is reflexive.

theorem Imperative.Trace.mayDropEvents_insertsTrueAssumes_append {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {a a' b b' : Trace P} (ha : RComp MayDropEvents (InsertsTrueAssumes allowed) a a') (hb : RComp MayDropEvents (InsertsTrueAssumes allowed) b b') : RComp MayDropEvents (InsertsTrueAssumes allowed) (a ++ b) (a' ++ b')

Dropping events, then inserting true assumptions, is closed under concatenation.

theorem Imperative.Trace.mayDropEvents_insertsTrueAssumes_drop_left {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} (a : Trace P) {b b' : Trace P} (h : RComp MayDropEvents (InsertsTrueAssumes allowed) b b') : RComp MayDropEvents (InsertsTrueAssumes allowed) (a ++ b) b'

Dropping a whole prefix of the source keeps dropping events, then inserting true assumptions.

theorem Imperative.Trace.mayDropEvents_insertsTrueAssumes_mono {P : PureExpr} [HasBool P] {allowed allowed' : P.Factory → Prop} (hmono : ∀ (F : P.Factory), allowed F → allowed' F) {t t' : Trace P} (h : RComp MayDropEvents (InsertsTrueAssumes allowed) t t') : RComp MayDropEvents (InsertsTrueAssumes allowed') t t'

Dropping events, then inserting true assumptions under some allowed factories, relates the same traces under any larger set of allowed factories.

theorem Imperative.Trace.mayDropEvents_insertsTrueAssumes_assumptionsHold {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {I : ConditionInterp P} (htrue : I.TrueStutterHolds allowed) {t t' : Trace P} (h : RComp MayDropEvents (InsertsTrueAssumes allowed) t t') {w : I.World} (hA : AssumptionsHold P I w t) : AssumptionsHold P I w t'

The assumptions of a trace related to t by dropping events, then inserting true assumptions, hold in every world where those of t hold, when every operationally true condition under an allowed factory holds in every world.

theorem Imperative.Trace.InsertsAsserts.mono_allowed {P : PureExpr} [HasBool P] {allowed allowed' : P.Factory → Prop} (hmono : ∀ (F : P.Factory), allowed F → allowed' F) {t t' : Trace P} (h : InsertsAsserts allowed t t') : InsertsAsserts allowed' t t'

Inserting assertions under some allowed factories inserts them under any larger set of allowed factories.

theorem Imperative.Trace.InsertsAsserts.reflect {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) {keep : EventArg P → Prop} (hkeep : ∀ (a b : EventArg P), b.label = a.label → b.metadata = a.metadata → keep a → keep b) {t t' : Trace P} (h : InsertsAsserts allowed t t') {A A' : Trace P} : (∀ (w : I.World), AssumptionsHold P I w A → AssumptionsHold P I w A') → AssertionsValidFromP P I keep A' t' → AssertionsValidFromP P I keep A t ∧ ∀ (w : I.World), AssumptionsHold P I w A → AssumptionsHold P I w t → AssumptionsHold P I w t'

Reflecting validity across inserted assertions. For an interpretation I under which conditions with the same value hold alike under allowed factories (EventArg.SameValue), and a filter keep of assertions that depends only on label and metadata: when the target t' keeps keep valid after the assumptions A', and A' holds where A does, then t keeps keep valid after A, and the assumptions of t' hold where those of A and t do.

theorem Imperative.Trace.InsertsAsserts.assertionsValidFromP_reflect {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) {keep : EventArg P → Prop} (hkeep : ∀ (a b : EventArg P), b.label = a.label → b.metadata = a.metadata → keep a → keep b) {t t' : Trace P} (h : InsertsAsserts allowed t t') (hv : AssertionsValidFromP P I keep [] t') : AssertionsValidFromP P I keep [] t

Under an interpretation for which conditions with the same value hold alike under allowed factories, the validity of the assertions of the target satisfying keep implies that of the assertions of the source satisfying keep, for a filter keep depending only on label and metadata.

theorem Imperative.Trace.InsertsAsserts.reachable_transfer {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) {t t' : Trace P} (h : InsertsAsserts allowed t t') (hr : Reachable P I t) : Reachable P I t'

Under an interpretation for which conditions with the same value hold alike under allowed factories, the target is reachable where the source is.

theorem Imperative.Trace.InsertsCheckedAssumes.mono_allowed {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {Checks : EventArg P → Prop} {allowed' : P.Factory → Prop} (hmono : ∀ (F : P.Factory), allowed F → allowed' F) {before t t' : Trace P} (h : InsertsCheckedAssumes allowed Checks before t t') : InsertsCheckedAssumes allowed' Checks before t t'

Inserting checked assumptions under some allowed factories inserts them under any larger set of allowed factories.

theorem Imperative.Trace.InsertsCheckedAssumes.reflect {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {Checks : EventArg P → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) (htrue : I.TrueStutterHolds allowed) {keep : EventArg P → Prop} {before t t' : Trace P} (h : InsertsCheckedAssumes allowed Checks before t t') {A A' : Trace P} : (∀ (c : EventArg P), Event.assert c ∈ before → Checks c → ∀ (w : I.World), AssumptionsHold P I w A' → I.holds w c) → (∀ (w : I.World), AssumptionsHold P I w A → AssumptionsHold P I w A') → AssertionsValidFromP P I (fun (c : EventArg P) => Checks c ∨ keep c) A' t' → AssertionsValidFromP P I keep A t ∧ ∀ (w : I.World), AssumptionsHold P I w A → AssumptionsHold P I w t → AssumptionsHold P I w t'

Reflecting validity across inserted checked assumptions. For an interpretation I under which conditions with the same value hold alike and true conditions hold, both under allowed factories: when the target t' keeps (Checks c ∨ keep c) valid after the assumptions A', its checking assertions before it hold where A' does, and A' holds where A does, then t keeps keep valid after A, and the assumptions of t' hold where those of A and t do.

theorem Imperative.Trace.InsertsCheckedAssumes.assertionsValidFromP_reflect {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {Checks : EventArg P → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) (htrue : I.TrueStutterHolds allowed) {keep : EventArg P → Prop} {t t' : Trace P} (h : InsertsCheckedAssumes allowed Checks [] t t') (hv : AssertionsValidFromP P I (fun (c : EventArg P) => Checks c ∨ keep c) [] t') : AssertionsValidFromP P I keep [] t

Under an interpretation for which conditions with the same value hold alike and true conditions hold, under allowed factories, the validity of the assertions of the target satisfying Checks or keep implies that of the assertions of the source satisfying keep.

theorem Imperative.Trace.InsertsCheckedAssumes.reachable_transfer {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {Checks : EventArg P → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) (htrue : I.TrueStutterHolds allowed) {t t' : Trace P} (h : InsertsCheckedAssumes allowed Checks [] t t') (hv : AssertionsValidFromP P I Checks [] t') (hr : Reachable P I t) : Reachable P I t'

Under an interpretation for which conditions with the same value hold alike and true conditions hold, under allowed factories, the target is reachable where the source is, when its assertions satisfying Checks are valid.

theorem Imperative.Trace.insertsAsserts_insertsCheckedAssumes_mono {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {Checks : EventArg P → Prop} {allowed' : P.Factory → Prop} (hmono : ∀ (F : P.Factory), allowed F → allowed' F) {t t' : Trace P} (h : RComp (InsertsAsserts allowed) (InsertsCheckedAssumes allowed Checks []) t t') : RComp (InsertsAsserts allowed') (InsertsCheckedAssumes allowed' Checks []) t t'

Inserting assertions, then checked assumptions, under some allowed factories, relates the same traces under any larger set of allowed factories.

theorem Imperative.Trace.insertsAsserts_insertsCheckedAssumes_assertionsValidFromP_reflect {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {Checks : EventArg P → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) (htrue : I.TrueStutterHolds allowed) {keep : EventArg P → Prop} (hkeep : ∀ (a b : EventArg P), b.label = a.label → b.metadata = a.metadata → keep a → keep b) {t t' : Trace P} (h : RComp (InsertsAsserts allowed) (InsertsCheckedAssumes allowed Checks []) t t') (hv : AssertionsValidFromP P I (fun (c : EventArg P) => Checks c ∨ keep c) [] t') : AssertionsValidFromP P I keep [] t

Validity reflected across inserted assertions and then checked assumptions. Under an interpretation for which conditions with the same value hold alike and true conditions hold, under allowed factories, the validity of the assertions of the target satisfying Checks or keep implies that of the assertions of the source satisfying keep, for a filter keep depending only on label and metadata.

theorem Imperative.Trace.insertsAsserts_insertsCheckedAssumes_assertionsValid_reflect {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {Checks : EventArg P → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) (htrue : I.TrueStutterHolds allowed) {t t' : Trace P} (h : RComp (InsertsAsserts allowed) (InsertsCheckedAssumes allowed Checks []) t t') (hv : AssertionsValid P I t') : AssertionsValid P I t

Under an interpretation for which conditions with the same value hold alike and true conditions hold, under allowed factories, the validity of the assertions of the target implies that of the assertions of the source, across inserted assertions and then checked assumptions.

theorem Imperative.Trace.insertsAsserts_insertsCheckedAssumes_reachable_transfer {P : PureExpr} [HasBool P] {allowed : P.Factory → Prop} {Checks : EventArg P → Prop} {I : ConditionInterp P} (hstable : I.StableUnder (EventArg.SameValue allowed)) (htrue : I.TrueStutterHolds allowed) {t t' : Trace P} (h : RComp (InsertsAsserts allowed) (InsertsCheckedAssumes allowed Checks []) t t') (hv : AssertionsValidFromP P I Checks [] t') (hr : Reachable P I t) : Reachable P I t'

Under an interpretation for which conditions with the same value hold alike and true conditions hold, under allowed factories, the target is reachable where the source is, across inserted assertions and then checked assumptions, when the assertions of the target satisfying Checks are valid.

theorem Imperative.Trace.PreservesLastEvent.append_left {P : PureExpr} {R : Trace P → Trace P → Prop} (happ : ∀ {a a' b b' : Trace P}, R a a' → R b b' → R (a ++ b) (a' ++ b')) {a a' b b' : Trace P} (ha : R a a') (hb : PreservesLastEvent R b b') (hne : b' ≠ []) : PreservesLastEvent R (a ++ b) (a' ++ b')

A relation closed under concatenation, relating a to a', followed by a nonempty target preserving the last event of b, preserves the last event of a ++ b.

theorem Imperative.Trace.PreservesLastEvent.reflectsLastAssertion {P : PureExpr} {I : ConditionInterp P} {R : Trace P → Trace P → Prop} {Extra : Trace P → Prop} (hR : ∀ {t t' : Trace P} {w : I.World}, R t t' → AssumptionsHold P I w t → AssumptionsHold P I w t') : ReflectsLastAssertion I (HasExtraEvents (PreservesLastEvent R) Extra)

A relation R carrying assumption satisfaction from source to target: a target preserving the last event of the source, after events related by R, followed by any extra events, reflects last assertions.