Persistent semantic choice inputs at actual source random-call sites. This is input data, not a MIR/state/execution representation or a PRNG seed. Every successful request consumes exactly one fresh typed entry.
@[instance_reducible]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
@[instance_reducible]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
- floatUlp : IntegerSite
Instances For
@[instance_reducible]
@[instance_reducible]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
@[instance_reducible]
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
Exact source request and its support, retained for each consumed choice. A diagnostic trace is one concrete execution, not a claim that other legal source outcomes have been checked.
- index (site : IndexSite) (count : Nat) : Request
- boolean (site : BoolSite) : Request
- bernoulli (site : BoolSite) (rateBits : UInt64) : Request
- integer (site : IntegerSite) (lower upper : Int) : Request
- bytes (site : ByteSite) (length : Nat) : Request
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
Strict finite input remains the default. boundedDiagnostic opts into
generating a domain-valid choice only when supplied inputs run out. Its bounds
cap generated draws and the length of each generated byte vector.
- strict : Policy
- boundedDiagnostic (maxGeneratedChoices maxByteLength : Nat) : Policy
- boundedSeededDiagnostic
(maxGeneratedChoices maxByteLength : Nat)
(seed : UInt64)
: Policy
Deterministic seeded diagnostic draws. This is a replay aid for exploring one trace, not rand/Miri PRNG equivalence or exhaustive exploration.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Miri.Interpreter.ExecutionChoices.instDecidableEqPolicy.decEq Miri.Interpreter.ExecutionChoices.Policy.strict Miri.Interpreter.ExecutionChoices.Policy.strict = isTrue ⋯
Instances For
@[instance_reducible]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
Instances For
def
Miri.Interpreter.ExecutionChoices.index
{S : Type}
(access : Access S)
(site : IndexSite)
(count : Nat)
:
Count is the exact source candidate support, not the number of all stores or threads. An empty source candidate domain fails before examining the tape.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.ExecutionChoices.bernoulli
{S : Type}
(access : Access S)
(site : BoolSite)
(rateBits : UInt64)
:
Restrict support to the exact rand 0.10.3 Bernoulli threshold
floor(p * 2^64): true is possible iff that threshold is nonzero, and false
is possible iff it is less than 2^64. This also handles probabilities too
small to admit any true sample.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.ExecutionChoices.integer
{S : Type}
(access : Access S)
(site : IntegerSite)
(lower upper : Int)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.ExecutionChoices.bytes
{S : Type}
(access : Access S)
(site : ByteSite)
(length : Nat)
:
A source fill_bytes/getrandom draw is consumed before the physical write. The full vector is one choice; no PRNG seed or per-byte reused selector exists.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Miri.Interpreter.ExecutionChoices.through
{T S : Type}
(outerGet : T → S)
(outerPut : T → S → T)
(inner : Access S)
:
Access T
Compose a tape lens through an owner's existing state; all actual memory, clock, stack and provenance fields remain in that one state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
- payload : Payload
- choices : Tape
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Miri.Interpreter.ExecutionChoices.index_supplied
{S : Type}
(access : Access S)
(state : S)
(tape : Tape)
(site : IndexSite)
(count value : Nat)
(current : access.get state = tape)
(strict : tape.policy = Policy.strict)
(input : tape.inputs[tape.cursor]? = some (Input.index site value))
(supported : value < count)
:
index access site count state = EStateM.Result.ok value
(access.put state
{ inputs := tape.inputs, cursor := tape.cursor + 1, policy := tape.policy,
generatedChoices := tape.generatedChoices, diagnosticRngState := tape.diagnosticRngState,
events := tape.events.push { request := Request.index site count, input := Input.index site value } })
Exact supplied typed index input, with no diagnostic generation or seed. The hypotheses describe raw input data and the index's complete legal support.
theorem
Miri.Interpreter.ExecutionChoices.bernoulli_supplied
{S : Type}
(access : Access S)
(state : S)
(tape : Tape)
(site : BoolSite)
(rate : UInt64)
(value validFalse : Bool)
(current : access.get state = tape)
(strict : tape.policy = Policy.strict)
(input : tape.inputs[tape.cursor]? = some (Input.boolean site value))
(probability : TerminatorMachine.permitsPreemption rate false = Except.ok validFalse)
(supported : TerminatorMachine.permitsPreemption rate value = Except.ok true)
:
bernoulli access site rate state = EStateM.Result.ok value
(access.put state
{ inputs := tape.inputs, cursor := tape.cursor + 1, policy := tape.policy,
generatedChoices := tape.generatedChoices, diagnosticRngState := tape.diagnosticRngState,
events := tape.events.push { request := Request.bernoulli site rate, input := Input.boolean site value } })
Exact supplied Bernoulli input with the actual source threshold support. Even a probability-zero/one request consumes its typed response.
Public proof boundary for the existing diagnostic calculation.
Equations
Instances For
def
Miri.Interpreter.ExecutionChoices.diagnosticInputSource
{S : Type}
(request : Request)
(maxByteLength : Nat)
:
Equations
- Miri.Interpreter.ExecutionChoices.diagnosticInputSource request maxByteLength = Miri.Interpreter.ExecutionChoices.diagnosticInput✝ request maxByteLength
Instances For
theorem
Miri.Interpreter.ExecutionChoices.index_supplied_any_policy
{S : Type}
(access : Access S)
(state : S)
(tape : Tape)
(site : IndexSite)
(count value : Nat)
(current : access.get state = tape)
(input : tape.inputs[tape.cursor]? = some (Input.index site value))
(supported : value < count)
:
index access site count state = EStateM.Result.ok value
(access.put state
{ inputs := tape.inputs, cursor := tape.cursor + 1, policy := tape.policy,
generatedChoices := tape.generatedChoices, diagnosticRngState := tape.diagnosticRngState,
events := tape.events.push { request := Request.index site count, input := Input.index site value } })
A supported supplied head bypasses policy generation under every policy. The raw head also rules out the diagnostic cursor-before-prefix error.
theorem
Miri.Interpreter.ExecutionChoices.bernoulli_supplied_any_policy
{S : Type}
(access : Access S)
(state : S)
(tape : Tape)
(site : BoolSite)
(rate : UInt64)
(value validFalse : Bool)
(current : access.get state = tape)
(input : tape.inputs[tape.cursor]? = some (Input.boolean site value))
(probability : TerminatorMachine.permitsPreemption rate false = Except.ok validFalse)
(supported : TerminatorMachine.permitsPreemption rate value = Except.ok true)
:
bernoulli access site rate state = EStateM.Result.ok value
(access.put state
{ inputs := tape.inputs, cursor := tape.cursor + 1, policy := tape.policy,
generatedChoices := tape.generatedChoices, diagnosticRngState := tape.diagnosticRngState,
events := tape.events.push { request := Request.bernoulli site rate, input := Input.boolean site value } })
theorem
Miri.Interpreter.ExecutionChoices.diagnosticInputSource_index
{S : Type}
(site : IndexSite)
(count maxByteLength : Nat)
:
diagnosticInputSource (Request.index site count) maxByteLength = have __do_jp := fun (__r : Unit) => pure (Input.index site 0);
if (count == 0) = true then do
let __r ← throw (StepError.resourceExhaustion "diagnostic choice has empty index support")
__do_jp __r
else __do_jp ()
theorem
Miri.Interpreter.ExecutionChoices.diagnosticInputSource_bernoulli
{S : Type}
(site : BoolSite)
(rateBits : UInt64)
(maxByteLength : Nat)
:
diagnosticInputSource (Request.bernoulli site rateBits) maxByteLength = have __do_jp := fun (falseAllowed : Bool) =>
if falseAllowed = true then pure (Input.boolean site false)
else have __do_jp := fun (trueAllowed : Bool) =>
if trueAllowed = true then pure (Input.boolean site true)
else throw (StepError.resourceExhaustion "diagnostic choice has empty Bernoulli support");
match TerminatorMachine.permitsPreemption rateBits true with
| Except.ok allowed => do
let trueAllowed ← pure allowed
__do_jp trueAllowed
| Except.error error => do
let trueAllowed ← throw error
__do_jp trueAllowed;
match TerminatorMachine.permitsPreemption rateBits false with
| Except.ok allowed => do
let falseAllowed ← pure allowed
__do_jp falseAllowed
| Except.error error => do
let falseAllowed ← throw error
__do_jp falseAllowed
theorem
Miri.Interpreter.ExecutionChoices.seededDiagnosticInputSource_index
{S : Type}
(site : IndexSite)
(count maxByteLength : Nat)
(seed state : UInt64)
(firstGenerated : Bool)
:
seededDiagnosticInputSource (Request.index site count) maxByteLength seed state firstGenerated = have state := if firstGenerated = true then seed else state;
have __do_jp := fun (__r : Unit) =>
match nextDiagnosticWordSource state with
| (word, next) => pure (Input.index site (word.toNat % count), next);
if (count == 0) = true then do
let __r ← throw (StepError.resourceExhaustion "diagnostic choice has empty index support")
__do_jp __r
else __do_jp ()
theorem
Miri.Interpreter.ExecutionChoices.seededDiagnosticInputSource_bernoulli
{S : Type}
(site : BoolSite)
(rateBits : UInt64)
(maxByteLength : Nat)
(seed state : UInt64)
(firstGenerated : Bool)
:
seededDiagnosticInputSource (Request.bernoulli site rateBits) maxByteLength seed state firstGenerated = have state := if firstGenerated = true then seed else state;
have __do_jp := fun (falseAllowed : Bool) =>
have __do_jp := fun (trueAllowed : Bool) =>
have __do_jp := fun (__r : Unit) =>
match nextDiagnosticWordSource state with
| (word, next) =>
if (!falseAllowed) = true then pure (Input.boolean site true, next)
else if (!trueAllowed) = true then pure (Input.boolean site false, next)
else have __do_jp := fun (decoded : FloatDecoded) =>
match decoded.value with
| FloatClass.finite numerator denominator =>
have threshold := numerator * 2 ^ 64 / denominator;
pure (Input.boolean site (decide (word.toNat < threshold)), next)
| x => throw (StepError.invalidProgram "diagnostic Bernoulli probability is nonfinite");
match { format := FloatFormat.binary64, bits := BitVec.ofNat 128 rateBits.toNat }.decode with
| Except.ok value => do
let decoded ← pure value
__do_jp decoded
| Except.error error => do
let decoded ←
throw
(StepError.invalidProgram
(toString "diagnostic Bernoulli probability encoding: " ++ toString (reprStr error)))
__do_jp decoded;
if (falseAllowed || trueAllowed) = true then __do_jp ()
else do
let __r ← throw (StepError.resourceExhaustion "diagnostic choice has empty Bernoulli support")
__do_jp __r;
match TerminatorMachine.permitsPreemption rateBits true with
| Except.ok allowed => do
let trueAllowed ← pure allowed
__do_jp trueAllowed
| Except.error error => do
let trueAllowed ← throw error
__do_jp trueAllowed;
match TerminatorMachine.permitsPreemption rateBits false with
| Except.ok allowed => do
let falseAllowed ← pure allowed
__do_jp falseAllowed
| Except.error error => do
let falseAllowed ← throw error
__do_jp falseAllowed
def
Miri.Interpreter.ExecutionChoices.demandSource
{S : Type}
(access : Access S)
(request : Request)
:
Equations
- Miri.Interpreter.ExecutionChoices.demandSource access request = Miri.Interpreter.ExecutionChoices.demand✝ access request
Instances For
theorem
Miri.Interpreter.ExecutionChoices.demandSource_eq
{S : Type}
(access : Access S)
(request : Request)
:
demandSource access request = do
let __do_lift ← get
have tape : Tape := access.get __do_lift
have __do_jp : Unit → M S Input := fun (__r : Unit) =>
match tape.inputs[tape.cursor]? with
| some value => pure value
| x =>
match tape.policy with
| Policy.strict => Miri.Interpreter.ExecutionChoices.unknown✝ "tape exhausted"
| Policy.boundedDiagnostic maxChoices maxByteLength =>
have __do_jp := fun (__r : Unit) => do
let value ← diagnosticInputSource request maxByteLength
modify fun (state : S) =>
have current := access.get state;
access.put state
{ inputs := current.inputs.push value, cursor := current.cursor, policy := current.policy,
generatedChoices := current.generatedChoices + 1, diagnosticRngState := current.diagnosticRngState,
events := current.events }
pure value;
if tape.generatedChoices ≥ maxChoices then do
let __r ← throw (StepError.resourceExhaustion "bounded diagnostic choice count exhausted")
__do_jp __r
else __do_jp ()
| Policy.boundedSeededDiagnostic maxChoices maxByteLength seed =>
have __do_jp := fun (__r : Unit) => do
let __x ←
seededDiagnosticInputSource request maxByteLength seed tape.diagnosticRngState (tape.generatedChoices == 0)
match __x with
| (value, nextState) => do
modify fun (state : S) =>
have current := access.get state;
access.put state
{ inputs := current.inputs.push value, cursor := current.cursor, policy := current.policy,
generatedChoices := current.generatedChoices + 1, diagnosticRngState := nextState,
events := current.events }
pure value;
if tape.generatedChoices ≥ maxChoices then do
let __r ← throw (StepError.resourceExhaustion "bounded seeded diagnostic choice count exhausted")
__do_jp __r
else __do_jp ()
if tape.cursor > tape.inputs.size then
match tape.policy with
| Policy.strict => __do_jp ()
| Policy.boundedDiagnostic maxGeneratedChoices maxByteLength => do
let __r ← throw (StepError.invalidProgram "diagnostic choice cursor exceeds supplied input prefix")
__do_jp __r
| Policy.boundedSeededDiagnostic maxGeneratedChoices maxByteLength seed => do
let __r ← throw (StepError.invalidProgram "diagnostic choice cursor exceeds supplied input prefix")
__do_jp __r
else __do_jp ()
theorem
Miri.Interpreter.ExecutionChoices.index_from_demand
{S : Type}
(access : Access S)
(state middle : S)
(tape : Tape)
(site : IndexSite)
(count value : Nat)
(source : demandSource access (Request.index site count) state = EStateM.Result.ok (Input.index site value) middle)
(current : access.get middle = tape)
(supported : value < count)
:
index access site count state = EStateM.Result.ok value
(access.put middle
{ inputs := tape.inputs, cursor := tape.cursor + 1, policy := tape.policy,
generatedChoices := tape.generatedChoices, diagnosticRngState := tape.diagnosticRngState,
events := tape.events.push { request := Request.index site count, input := Input.index site value } })
theorem
Miri.Interpreter.ExecutionChoices.bernoulli_from_demand
{S : Type}
(access : Access S)
(state middle : S)
(tape : Tape)
(site : BoolSite)
(rate : UInt64)
(value validFalse : Bool)
(source : demandSource access (Request.bernoulli site rate) state = EStateM.Result.ok (Input.boolean site value) middle)
(current : access.get middle = tape)
(probability : TerminatorMachine.permitsPreemption rate false = Except.ok validFalse)
(supported : TerminatorMachine.permitsPreemption rate value = Except.ok true)
:
bernoulli access site rate state = EStateM.Result.ok value
(access.put middle
{ inputs := tape.inputs, cursor := tape.cursor + 1, policy := tape.policy,
generatedChoices := tape.generatedChoices, diagnosticRngState := tape.diagnosticRngState,
events := tape.events.push { request := Request.bernoulli site rate, input := Input.boolean site value } })