sync: engine v12.19 baseline (96 commits) - #88

Merged

dcccrypto merged 99 commits into

mainfrom

sync/v12.19-engine

Apr 28, 2026

Commits on Apr 17, 2026

feat: implement v12.18 admission-pair + sticky h_max + touch acceleration

aeyakovenko
and
claude
committed
feat: add v12.18 admission/acceleration Kani proofs

aeyakovenko
and
claude
committed
fix: integrate admit_outstanding_reserve_on_touch into touch lifecycle

aeyakovenko
and
claude
committed
fix: validate_admission_pair rejects admit_h_max == 0 (Bug 9)

aeyakovenko
and
claude
committed
fix: dt envelope + degenerate resolve branch (Bugs 1 & 2)

aeyakovenko
and
claude
committed
fix: Bug 92 + Bug 73 + Kani proofs K-71 + K-104 (Pass 2 audit)

aeyakovenko
and
claude
committed
fix: Bugs 3, 4, 5, 6, 9 from v12.18.1 pass 3 audit

aeyakovenko
and
claude
committed
fix: Pass 3 cleanup — record_uninsured_protocol_loss + dead code + checked_add

aeyakovenko
and
claude
committed
proofs: strengthen weak/vacuous proofs identified in substantiveness audit

aeyakovenko
and
claude
committed
proofs: fix resolve-bypass tests + strengthen counter tracking

aeyakovenko
and
claude
committed
proofs: fix 24 test failures after v12.18 + envelope + fail-conservative changes

aeyakovenko
and
claude
committed
v12.18.1 opening-fee/materialization removal (spec item 1)

aeyakovenko
and
claude
committed
v12.18.1 per-market active-position cap (spec item 2)

aeyakovenko
and
claude
committed
v12.18.1 uninsured-loss bookkeeping no-op (spec item 3)

aeyakovenko
and
claude
committed
v12.18.1 reserve validation ordering + bounds (spec item 4)

aeyakovenko
and
claude
committed
v12.18.1 fallible sticky-admission helper (spec item 5)

aeyakovenko
and
claude
committed
v12.18.1 API surface tightening + keeper_crank clamp→error (items 8-9)

aeyakovenko
and
claude
committed
v12.18.1 public endpoint postcondition checks (item 7)

aeyakovenko
and
claude
committed
v12.18.1 resolved semantics spec-exactness (item 6)

aeyakovenko
and
claude
committed
proofs: strengthen admission/postcondition/keeper_crank coverage

aeyakovenko
and
claude
committed
v12.18.1 reserve atomicity + deposit_fee_credits + O(1) materialize

aeyakovenko
and
claude
committed
proofs: close remaining reserve-validation gaps (reviewer pass)

aeyakovenko
and
claude
committed
tests: strengthen assertions in added Kani + unit tests

aeyakovenko
and
claude
committed
fix: resolve band check always runs + deposit_fee_credits rejects overpay

aeyakovenko
and
claude
committed
fix: free_slot capital/fee_credits checks + init_in_place full canon + new_with_market gated

aeyakovenko
and
claude
committed

Commits on Apr 18, 2026

Commits on Apr 19, 2026

Commits on Apr 20, 2026

feat: add small/medium slab capacity feature flags

aeyakovenko
and
claude
committed

Commits on Apr 22, 2026

Commits on Apr 23, 2026

Commits on Apr 24, 2026

Commits on Apr 25, 2026

Commits on Apr 26, 2026

Document price movement bound invariant

aeyakovenko
authored and
dcccrypto
committed
Rewrite README around three invariants

aeyakovenko
authored and
dcccrypto
committed