Replay-Buffer Proofs #
These theorems certify the structural guarantees that make the runtime replay buffer safe to use:
- empty buffers really have size zero;
- zero-capacity buffers remain empty after a push;
- pushing below capacity increments size;
- pushing at capacity preserves the configured capacity by evicting the oldest element.
This is the proof layer for the "bounded FIFO" invariant used by DQN-style replay.
@[simp]
theorem
Proofs.RL.Replay.empty_items_size
{α : Type}
{obsShape : Spec.Shape}
{nActions : ℕ}
(capacity : ℕ)
:
Empty replay buffers contain no stored transitions.
@[simp]
theorem
Proofs.RL.Replay.empty_size
{α : Type}
{obsShape : Spec.Shape}
{nActions : ℕ}
(capacity : ℕ)
:
Empty replay buffers report size zero through the public size helper.
@[simp]
theorem
Proofs.RL.Replay.push_capacity_zero_items_size
{α : Type}
{obsShape : Spec.Shape}
{nActions : ℕ}
(b : Runtime.RL.Replay.Buffer α obsShape nActions)
(t : Runtime.RL.Replay.Transition α obsShape nActions)
(hcap : b.capacity = 0)
:
A zero-capacity replay buffer remains empty after any push.
theorem
Proofs.RL.Replay.push_size_of_room
{α : Type}
{obsShape : Spec.Shape}
{nActions : ℕ}
(b : Runtime.RL.Replay.Buffer α obsShape nActions)
(t : Runtime.RL.Replay.Transition α obsShape nActions)
(hroom : b.items.size + 1 ≤ b.capacity)
:
If there is room for one more item, push increases the size by exactly one.
theorem
Proofs.RL.Replay.push_size_of_full
{α : Type}
{obsShape : Spec.Shape}
{nActions : ℕ}
(b : Runtime.RL.Replay.Buffer α obsShape nActions)
(t : Runtime.RL.Replay.Transition α obsShape nActions)
(hcap : 0 < b.capacity)
(hfull : b.items.size = b.capacity)
:
If the buffer is exactly full and has positive capacity, push preserves size by evicting one old
item and appending the new one.