Lef/circular buffer#554

Open

elefthei wants to merge 27 commits into

mainfrom

lef/circular_buffer

Commits on Feb 8, 2026

Commits on Feb 9, 2026

Simplify CircularBuffer proof bodies
elefthei
committed

Commits on Feb 11, 2026

Outer box instead of inner boxes
elefthei
committed

Commits on Feb 14, 2026

More general AVL trees, more complete proof of CircularBuffer
elefthei
committed

Commits on Feb 18, 2026

Refactor CircularBuffer to single RM-tracked predicate

elefthei
and
Copilot
committed
Add RecvBufferWrapper.fst for Karamel extraction

elefthei
and
Copilot
committed

Commits on Feb 19, 2026