Effectful source-ordered Tree Borrows reborrow core. Compiler request values are shared with the legacy pure fixture API; precomputed hooks.dataRace values are deliberately not consulted by this engine.

inductive Miri.TreeBorrows.RetagPipeline.Effectful.Error (HookError : Type) : Type

• core {HookError : Type} (error : RetagPipeline.Error) : Error HookError
• hook {HookError : Type} (error : HookError) : Error HookError

def Miri.TreeBorrows.RetagPipeline.Effectful.instReprError.repr {HookError✝ : Type} [Repr HookError✝] : Error HookError✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.TreeBorrows.RetagPipeline.Effectful.instReprError {HookError✝ : Type} [Repr HookError✝] : Repr (Error HookError✝)

Equations

• Miri.TreeBorrows.RetagPipeline.Effectful.instReprError = { reprPrec := Miri.TreeBorrows.RetagPipeline.Effectful.instReprError.repr }

structure Miri.TreeBorrows.RetagPipeline.Effectful.Transition (External HookError : Type) : Type

A concurrency leaf changes external clock/store state, never the borrowed Tree Borrows allocation itself. All changes before errors remain available.

• external : External
• outcome : Except HookError Unit

structure Miri.TreeBorrows.RetagPipeline.Effectful.Hooks (MachineKind External HookError : Type) : Type

• dataRace : Option (MachineState MachineKind → External → Memory.AllocId → AccessKind → Memory.AllocRange → Transition External HookError)

  None exactly when the allocation has no vector-clock model. A configured detector applies its own source race_detecting guard inside the callback.

structure Miri.TreeBorrows.RetagPipeline.Effectful.Result (MachineKind External HookError : Type) : Type

• state : MachineState MachineKind
• external : External
• outcome : Except (Error HookError) (Option Memory.Provenance)
• events : Array Event

def Miri.TreeBorrows.RetagPipeline.Effectful.retagPointerValue {MachineKind External HookError : Type} [DecidableEq MachineKind] (state : MachineState MachineKind) (request : Request) (external : External) (effects : Hooks MachineKind External HookError) : Result MachineKind External HookError

Source tb_retag_ptr_value followed by tb_retag_place and the allocation-local portion of tb_reborrow. Policy selection precedes place conversion; the dynamic-size query precedes new_ptr; pointer validation follows tag allocation. Hook failures return the state accumulated up to that source point, including installed protectors and earlier parent accesses.

Equations

• One or more equations did not get rendered due to their size.