Module effect_classification 

Oracle v1 effect classification.

For each built-in effect method covered by aver proof, this module records:

• Which proof dimension(s) it belongs to (snapshot / generative / output, and the combination generative + output used by e.g. Http.get).
• For snapshot and generative, the corresponding capability/oracle signature that lifted specs bind via given name: E.m = [...].

Output-only effects (for example Console.print, Time.sleep, and terminal drawing calls) are classified but do not have an oracle signature: they append to the per-branch trace segment and are asserted about via the trace API, not by binding an oracle in given.

The table is the single source of truth consumed by:

• given-clause type inference (given rnd: Random.int → oracle type (BranchPath, Int, Int, Int) -> Int).
• Lifting of effectful function bodies at proof-export time.
• Rejection diagnostics for unclassified effects.

Source of runtime signatures: src/services/*.rs and docs/services.md. Keep this table synchronized with the real built-ins.

Structs

EffectClassification

Classification of one effect method. runtime_params and runtime_return mirror the surface signature at call sites in user code; oracle signatures are derived from them (see oracle_signature).

Enums

EffectDimension

Proof dimension(s) an effect participates in. !-combinations are modelled directly rather than as flags for readability at call sites.

RuntimeType

Compact carrier for runtime signature components — kept separate from the full Type enum so the static table can live as a const array. Converted into Type on demand via [runtime_type].

Functions

classifications_for_proof_subset

Closed Oracle v1 proof-subset table, exposed for proof metadata generation. Callers must treat the returned slice as read-only metadata.

classify

Classify a built-in effect method, if it’s in Oracle v1’s closed set.

is_classified

Return true if the given name refers to an effect covered by Oracle v1.

is_verify_fabricable_handle

Opaque types that are runtime handles (id + connection metadata), not domain-invariant smart-constructor types. These may be fabricated inside verify-trace context so that Oracle stubs can return them without going through the live effect that normally produces them (e.g. Tcp.connect). All four soundness conditions from PR 221 apply:

oracle_signature

Oracle signature for use in lifted specs.