GenServer that owns the ETS tables for a single proof session.
Creates five shared, public tables on startup and keeps them alive for the
duration of the session tree. All other processes obtain the table references
via get_tables/1.
Tables created:
:stats— proof-search counters and timing metadata.:tombs— branch IDs that have been closed; used to poison descendants.:work_queue— ordered set of{priority_key, Branch.t()}entries.:idle_queue— branches parked waiting for iterative deepening.:traces— per-branch rule application history for proof reconstruction.:provenance— per-fresh-variable annotation (γ / prim-subst origin); seeShotTx.Prover.Provenance.:suggestions— instantiation hints published bySuggestionAgent, consumed by workers on splice; seeShotTx.Prover.Suggestion. Rows are{{prefix, recipe, term}, applied_count, %Suggestion{}}so that:ets.update_counter/3can enforce the cascade cap at position 2.
Summary
Functions
Returns a specification to start this module under a supervisor.
Returns the ETS table map for the given session_id.
Starts the ETS keeper for the given session_id.
Functions
Returns a specification to start this module under a supervisor.
See Supervisor.
Returns the ETS table map for the given session_id.
@spec start_link({String.t(), term()}) :: GenServer.on_start()
Starts the ETS keeper for the given session_id.