Explicit MIR producer settings and consumed-artifact identities. Source: Miri lib.rs::MIRI_DEFAULT_ARGS (190-211), bin/miri.rs driver setup; exporter producer.rs records actual compiler session settings and hashes the consumed crate artifacts. Comparison to a reference is conditional on that reference's provenance; it does not certify Rust behavior or establish UB freedom.

@[reducible, inline]

abbrev Miri.Input.ProducerEvidence.Result (α : Type u_1) : Type u_1

Equations

• Miri.Input.ProducerEvidence.Result = Except String

structure Miri.Input.ProducerEvidence.Artifact : Type

• path : String
• crateName : String
• kind : String
• sha256 : String
• sizeBytes : Nat
• withinSysroot : Bool
• sysrootRelativePath : Option String

structure Miri.Input.ProducerEvidence.Settings : Type

• sysrootPath : String
• sysrootManifestSha256 : String
• loadedArtifactsManifestSha256 : String
• requestedCfgMiri : Bool
• miriDefaultArgs : Array String
• rustcArgs : Array String
• effectivePanicStrategy : String
• requestedMirOptLevel : Option Nat
• mirEnablePasses : Array (String × Bool)
• mirPreserveUb : Bool
• extraConstUbChecks : Bool
• alwaysEncodeMir : Bool
• deduplicateDiagnostics : Bool
• artifacts : Array Artifact
• originalPayload : Lean.Json

def Miri.Input.ProducerEvidence.ofDocument (document : ImportDocumentCore) : Result Settings

Equations

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

def Miri.Input.ProducerEvidence.pinnedMiriDefaultArgs : Array String

Equations

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

def Miri.Input.ProducerEvidence.requestedCfgs (settings : Settings) : Array String

Retain every explicit cfg argument in its original compiler syntax. This does not infer built-in target cfgs from a target triple.

Equations

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

def Miri.Input.ProducerEvidence.compareReferenceInputs (actual reference : Settings) : Result Unit

Compare actual producer inputs to an independently pinned reference. Reference trust and source-to-MIR correctness remain explicit external assumptions. Both sysroot and non-sysroot consumed artifacts must match.

Equations

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