Module assumption 

Heuristic assumptions and proven knowledge shared by analysis passes.

A Proposition is a positive statement about the program (“function f returns to its caller”). During analysis each proposition can be in one of four states, tracked by a Truth in a single map on the Context:

• assumed true / assumed false — a pass guessed, recorded via Context::assume_true / assume_false. Assuming fails (returns false) if the opposite polarity is already assumed or known.
• known true / known false — proven by a verification pass via Context::set_known. Proving the opposite of an existing assumption records a Violation.

Every entry carries the name of the pass that recorded it, picked up automatically from the pass_scope thread-local set by the pipeline driver.

Because analysis passes mutate the Context arena in place, a violated assumption leaves behind IR that is now incorrect. The invalidation strategy is checkpoint + replay: a freshly-lifted baseline Context is cloned before any speculative analysis; after a round, if any violation was recorded (or a novel fact proven), the working copy is discarded, its known facts are seeded into a fresh clone, and the round replays. Knowledge only ever grows, so replay terminates.

Structs

AssumedCallEffect

The register-space effect the opt-in Proposition::AssumeCallingConvention hypothesis assigns to an indirect / unresolved call, precomputed once from the module’s calling convention by the assume_calling_convention pass and cached on the Shared context so the mem2reg / alias register classifier can consult it without an ABI in hand.

KnownContradiction

A proven fact that contradicted an existing known fact (as opposed to a mere assumption). Unlike a Violation, this is not a replay signal — it means two verification results, or a user-forced override and a verification result, disagree irreconcilably. The checkpoint+replay driver surfaces it as a hard error rather than looping.

PassName

A pass name, as recorded on truth-map entries. A transparent &'static str wrapper: serde’s derive would otherwise tie the deserializer lifetime to 'static, so it gets manual impls — serialized as a string, deserialized by leaking. Pass names form a small finite set, so the leak is bounded.

Truth

The recorded truth state of one Proposition.

Violation

A proven fact contradicting an earlier assumption — the signal that the checkpoint+replay driver must discard the working copy and replay.

Enums

Certainty

How certain we are about a proposition’s recorded value.

Proposition

A positive statement about the program whose truth a pass may assume or prove. Used as the key of the truth map on the Context.