ShotTx.Prover.Stats (ShotTx v0.0.1)

Lightweight ETS-backed counters/samplers for proof-session debugging, plus user-facing helpers to compile and pretty-print a snapshot.

Operates on the :stats table created by EtsKeeper. All ops are concurrency-safe and lock-free; samplers and max-trackers use CAS via :ets.select_replace/2.

Schema: {key, integer} # counters & max trackers {key, count, sum, min, max} # samplers {key, term} # one-off set/get (e.g. timestamps)

Summary

Types

report()

sampler()

snapshot()

tables()

Functions

compile(report)

Compiles a raw snapshot into a structured report grouped by category: :timing, :search, :rules, :branches, :csp.

duration_us(snapshot)

Total proof duration in microseconds, or nil if timing data is missing.

format(stats, opts \\ [])

Pretty-prints stats as a human-readable string. Accepts either a raw snapshot or a compiled report.

incr(tables, key, by \\ 1)

Atomic increment-or-create.

record_max(tables, key, value, retries \\ 3)

Best-effort max tracker. Retries on contention up to retries times.

record_sample(tables, key, value, retries \\ 3)

Records a sample. Maintains {count, sum, min, max} for the key.

set(tables, key, value)

One-shot set (non-atomic, used for timestamps / metadata).

snapshot(tables)

Snapshot the entire table as a map. Samplers expand to a stats map.

Types

report()

@type report() :: %{
  timing: map(),
  search: map(),
  rules: map(),
  branches: map(),
  csp: map()
}

sampler()

@type sampler() :: %{
  count: non_neg_integer(),
  sum: number(),
  min: number(),
  max: number(),
  avg: number()
}

snapshot()

@type snapshot() :: %{required(atom()) => integer() | sampler() | term()}

tables()

@type tables() :: %{stats: :ets.table()} | :ets.table()

Functions

compile(report)

@spec compile(snapshot() | report()) :: report()

Compiles a raw snapshot into a structured report grouped by category: :timing, :search, :rules, :branches, :csp.

Derived metrics included:

timing.duration_us / duration_ms from the start/finish timestamps.
search.steps_per_sec from steps_total and duration_us.
csp.success_rate from csp_calls_succeeded / csp_calls.

Idempotent: a compiled report passed in is returned unchanged.

duration_us(snapshot)

@spec duration_us(snapshot()) :: non_neg_integer() | nil

Total proof duration in microseconds, or nil if timing data is missing.

format(stats, opts \\ [])

@spec format(
  snapshot() | report(),
  keyword()
) :: String.t()

Pretty-prints stats as a human-readable string. Accepts either a raw snapshot or a compiled report.

Options:

:verbose (default false) — include rule/branch counters whose value is zero. By default they are hidden to reduce noise.
:sections (default :all) — subset of [:timing, :search, :rules, :branches, :csp] to render, in the given order.

incr(tables, key, by \\ 1)

@spec incr(tables(), atom(), integer()) :: integer()

Atomic increment-or-create.

record_max(tables, key, value, retries \\ 3)

@spec record_max(tables(), atom(), integer(), non_neg_integer()) :: :ok

Best-effort max tracker. Retries on contention up to retries times.

record_sample(tables, key, value, retries \\ 3)

@spec record_sample(tables(), atom(), number(), non_neg_integer()) :: :ok

Records a sample. Maintains {count, sum, min, max} for the key.

set(tables, key, value)

@spec set(tables(), atom(), term()) :: :ok

One-shot set (non-atomic, used for timestamps / metadata).

snapshot(tables)

@spec snapshot(tables()) :: snapshot()

Snapshot the entire table as a map. Samplers expand to a stats map.