05 — Bounded Proof Results

Methodology: single TX wrapped in BEGIN…ROLLBACK; pre-rollback state captured, then ROLLBACK reverts all data, then post-rollback state captured to confirm full restoration.

File: /root/dieu45-phase1/050-proof.sql (139 lines, 19 logical steps).

Verdict: PASS — every refusal fires, every transition happens, ROLLBACK restores 0/0/0 row state and false gate state.

Cases exercised

Step 1 — Gate-OFF refusal

fn_job_enqueue('phase1_proof_kind','phase1_proof_actor',...,'phase1-proof-idem-1',...);

Result:

{"refused": true, "reason": "queue.job_substrate.enabled=false", "job_id": null}

job_queue row count after refusal: 0 ✓

Step 2 — Enable gate (UPDATE 1)

SELECT key,value WHERE key='queue.job_substrate.enabled' → true (in-TX).

Step 3 — Three enqueues (different priorities + max_attempts)

seq	idempotency_key	priority	max_attempts	result
1	phase1-proof-idem-1	50	3	refused=false, duplicate=false, state=queued
2	phase1-proof-idem-2	100	3	refused=false, duplicate=false
3	phase1-proof-idem-3	100	1	refused=false, duplicate=false

Read-back: 3 rows, priorities 50/100/100 ordered correctly, max_attempts honored, all state='queued'.

Step 4 — Idempotency replay

fn_job_enqueue(...same idem-1...);

Result:

{"refused": false, "duplicate": true, "job_id": "<existing>", "state": "queued",
 "idempotency_key": "phase1-proof-idem-1"}

job_queue row count still 3 ✓ — no duplicate row created.

Step 5 — Payload denylist CHECK

fn_job_enqueue(..., '{"vector":[1,2,3]}'::jsonb, ...)

Caught at CHECK level (SAVEPOINT before_denylist; ... EXCEPTION WHEN check_violation THEN ...):

NOTICE: denylist case OK: CHECK violation caught (vector key blocked)

Step 6 — fn_job_claim SKIP LOCKED

fn_job_claim('proof_executor_1', NULL, 2)  → count=2
fn_job_claim('proof_executor_2', NULL, 5)  → count=1

After both calls:

state  | lease_owner       | cnt
leased | proof_executor_1  |   2
leased | proof_executor_2  |   1

Order observed: priority 50 first, then 100. SKIP LOCKED behavior correct.

Step 7 — Ack + lease_owner_mismatch

fn_job_ack(<exec_1's job>, 'proof_executor_1', 'proof success summary')
→ {"state":"succeeded", ...}

fn_job_ack(<exec_1's job>, 'wrong_executor', NULL)
→ {"refused": true, "reason":"lease_owner_mismatch", "expected":"proof_executor_1", "got":"wrong_executor"}

Step 8 — Transient fail → retry_waiting

fn_job_fail_or_retry(<job>, 'proof_executor_1', 'transient probe error', false)
→ {"state":"retry_waiting", "attempts":1, "backoff_sec":10, "max_attempts":3,
   "scheduled_at":"2026-05-26T11:21:06.094572+00:00"}

scheduled_at = now() + 10 s exactly (verified: sched_in_sec = 10 against now()).

Step 9 — Permanent fail → dead_letter

-- job idem-3 had max_attempts=1, leased by exec_2
fn_job_fail_or_retry(<idem-3>, 'proof_executor_2', 'permanent probe error', true)
→ {"state":"dead_letter", "attempts":1,
   "dead_letter":{"dead_letter_id":"fb52c075-…","moved_at":"…"}}

Read-back:

state          | count
dead_letter    |     1
retry_waiting  |     1
succeeded      |     1

job_dead_letter row: triage_status='pending', moved_by='proof_executor_2', final_error='permanent probe error'.

Step 10 — Heartbeat gate-OFF refusal

fn_queue_heartbeat_tick('proof_executor_1','external_worker','ok',NULL,NULL,'{}')
→ {"refused": true, "reason": "queue.heartbeat.enabled=false"}

queue_heartbeat rows: 0 ✓

Step 11 — Heartbeat ticks (counter increments)

After UPDATE dot_config SET value='true' WHERE key='queue.heartbeat.enabled':

call	executor	ticks_total
hb1	proof_executor_1	1
hb2	proof_executor_1	2
hb3_other	proof_executor_2	1

executor_name     | executor_kind   | ticks_total | last_tick_status
proof_executor_1  | external_worker |           2 | ok
proof_executor_2  | DOT             |           1 | warn

Step 12 — Heartbeat metadata denylist CHECK

NOTICE: hb denylist OK: CHECK violation caught (secret key blocked)

Step 13 — fn_queue_stale_check at default and custom thresholds

Backdated proof_executor_2.last_tick_at to now()-1h.

At threshold=300 (default): 1 stale executor (proof_executor_2, age 3600s). At threshold=30 (custom): 1 stale (same).

Step 14 — v_queue_health snapshot

substrate_enabled | heartbeat_enabled | worker_enabled | stale_threshold | …
true              | true              | false          | 300            | …
queued | leased | retry_waiting | dead_letter | succeeded | fresh | warning | stale | dlq_pending
0      | 0      | 1             | 1           | 1         | 1     | 0       | 1     | 1

All counts match the actual state at the time of the snapshot.

Step 15 — v_job_queue_backlog

job_kind              | state          | row_count | avg_attempts | max_attempts_seen
phase1_proof_kind     | retry_waiting  |         1 |         1.00 |                 1
phase1_proof_kind     | succeeded      |         1 |         0.00 |                 0
phase1_proof_kind_alt | dead_letter    |         1 |         1.00 |                 1

Step 16 — v_job_dead_letter_summary

job_kind              | triage_status | row_count | avg_attempts
phase1_proof_kind_alt | pending       |         1 |         1.00

Steps 17–19 — ROLLBACK and post-rollback verification

Pre-rollback:

t                | rows
job_queue        |    3
job_dead_letter  |    1
queue_heartbeat  |    2

After ROLLBACK:

t                | rows
job_queue        |    0
job_dead_letter  |    0
queue_heartbeat  |    0

All gates restored:

queue.heartbeat.enabled                 | false
queue.heartbeat.stale_threshold_seconds | 300
queue.job_substrate.enabled             | false
queue.lease.duration_sec                | 300
queue.notify.enabled                    | false
queue.retry.backoff_base_sec            | 10
queue.retry.max_attempts_default        | 5
queue.worker.enabled                    | false

Cleanup

None required — all data was inside the rolled-back transaction. No actor-tagged residue on disk.

Verdict

PASS on all 19 steps. The substrate behaves as designed under refusal, idempotency, parallel claim (SKIP LOCKED), state transitions (queued → leased → succeeded | retry_waiting | dead_letter), heartbeat upsert + stale-check, and CHECK denylist for the 10 forbidden payload keys.