Research proof index

Probability that the k-th log entry's output is HEq to a fixed value u₀ : spec.Range t₀. Unlike probEvent_log_entry_eq_le which matches the full sigma entry, this only constrains the output component. The bound uses hrange to get 1/|Range default|.

Per-pair collision bound: For any two positions in a loggingOracle trace with distinct inputs, the probability that their outputs are HEq-equal is ≤ 1/|C|. This is the core ROM property: distinct oracle inputs yield independent uniform outputs. The hrange hypothesis ensures |Range default| is minimal across all oracle indices, so the bound holds...

Requiring the colliding second completion to finish successfully can only decrease the path-first equal-answer collision probability.

Main forking lemma: the failure probability is bounded by 1 - acc * (acc / q - 1/h).

Quantitative Std.Do'.WP interpretation of OracleComp spec valued in ℝ≥0∞. The wpTrans is the existing MAlgOrdered.wp (i.e. expectation of post under evalDist); the EPost.nil argument is ignored since OracleComp has no first-class exception slot. The three WP axioms reduce to the existing MAlgOrdered.{wp_pure, wp_bind, wp_mono} equali...

Expected-growth resource bound for expectedQuerySlack. Like expectedQuerySlack_resource_le, but a charged query may grow the resource by more than one in support, as long as it grows by at most g in expectation under the handler. Growth queries grow the resource by at most one in support, and free queries never grow it. The accumulated slack of...