Upgrade Ibex/CAPD to Codac - #4

Open

kunalsheth wants to merge 79 commits into

cav26from

Commits on Dec 19, 2025

Create README.md
kunalsheth
authored
20a8f9e
Add CAPD contractor silent omission edge-case logs.
kunalsheth
committed
f90dfbf
Add Dockerfile build and README instructions.
kunalsheth
committed
bc9d4d0

Commits on Dec 25, 2025

Add missing statistics prints for `. A` and PM Dumps on execution branch for direct lemma additions without matching.
kunalsheth
committed
535dd8d

Commits on Dec 27, 2025

Commits on Dec 28, 2025

Commits on Dec 29, 2025

Commits on Jan 1, 2026

Commits on Jan 3, 2026

Commits on Jan 5, 2026

Commits on Jan 6, 2026

Slightly increase PM timeout for very-long-running lemmas.
kunalsheth
committed
27463ce

Commits on Jan 7, 2026

Make threshold value for fixed-point a macro.
kunalsheth
committed
0024251

Commits on Apr 26, 2026

Initialize claude code.
kunalsheth
committed
0684a4c

Commits on Apr 27, 2026

Commits on Apr 30, 2026

Simplify build: let Codac handle IBEX instead of separate ExternalProject

kunalsheth
and
claude
committed
2658a79

Commits on May 1, 2026

Fix Codac/IBEX migration: use pre-built binaries on macOS, fix CaDiCaL 3.0 API

kunalsheth
and
claude
committed
742720b

Commits on May 2, 2026

Implement Codac v2 ODE contractor (Lohner) and trajectory trace generation

kunalsheth
and
claude
committed
a21b7a4
Make it build on macOS, Ubuntu, arm, and x68.
kunalsheth
committed
667cee2

Commits on Jun 5, 2026

Replace LohnerAlgorithm hull loop with CtcLohner FWD_BWD for joint endpoint contraction

kunalsheth
and
claude
committed
2449835
Add docs/ directory with deep reference documentation

kunalsheth
and
claude
committed
06bab0c
Add lightweight benchmarking infrastructure and Claude skills

kunalsheth
and
claude
committed
0611600
Update benchmark skill to use background execution; record first anomalies

kunalsheth
and
claude
committed
00d38ea
Fix benchmark skill execution and anomaly selection

kunalsheth
and
claude
committed
43104cd
Overhaul benchmark infrastructure: SAR-ADC path fix, seamless baseline skill

kunalsheth
and
claude
committed
a5a3d9c
Limit benchmark parallelism to 12 concurrent jobs

kunalsheth
and
claude
committed
3e15986
Optimize Codac ODE + IBEX fwdbwd contractors

kunalsheth
and
claude
committed
a224767

Commits on Jun 6, 2026

Restore BWD ODE contractor; add ground-truth flip classifier + semantic tests

kunalsheth
and
claude
committed
a0fd9c8
Fix flow_cache_map pointer-reuse bug; remove test workaround

kunalsheth
and
claude
committed
fed8a02
Consolidate ODE migration docs; reject custom Taylor integrator option

kunalsheth
and
claude
committed
57d876d
Update CODAC_MIGRATION.md to reflect cache-key fix and item-5 attempt

kunalsheth
and
claude
committed
96fbd64

Commits on Jun 7, 2026

Reintroduce CAPD as gated second ODE contractor

kunalsheth
and
claude
committed
644bb56
Update docs to reflect CAPD re-integration as gated second ODE backend

kunalsheth
and
claude
committed
bd8a7ce
Switch benchmark infrastructure to PAR2 scoring

kunalsheth
and
claude
committed
66db1c7
Root-cause non-ODE slowdown to IBEX gradient overhead

kunalsheth
and
claude
committed
cdf8809
Document strategic decision to fork ibex-team/ibex-lib and eliminate Codac

kunalsheth
and
claude
committed
d814ec1

Commits on Jun 16, 2026

ibex: switch fork pin to GitHub URL; add log/pow soundness tests

kunalsheth
and
claude
committed
7a64db8
ode: eliminate Codac, make CAPD the sole ODE backend
kunalsheth
committed
f226e76
ibex: use Function::backward callback in fwdbwd contractor
kunalsheth
committed
b4a29fe
test: add regression test for ibex lazy-gradient patch
kunalsheth
committed
ff6fa9a
test: document mainline-vs-cav26 ibex FPU/gaol-init differences
kunalsheth
committed
7581ba5
filter_assertion: use named designator for .changed field
kunalsheth
committed
e374602
benchmark: refresh local baseline and state after Codac elimination
kunalsheth
committed
f9fa5f7

Commits on Jun 17, 2026

ode/sat: fix two benchmark crashes (CaDiCaL factor abort, CAPD param overrun)

kunalsheth
and
claude
committed
af600cd

Commits on Jun 18, 2026

contractor: guard FE_UPWARD in ibex fwdbwd Prune (fix false-UNSAT)

kunalsheth
and
claude
committed
ab27638
test: add ibex backward-callback regression tests (alias + partial-empty)

kunalsheth
and
claude
committed
bf0775d
benchmark: refresh local baseline and anomaly state

kunalsheth
and
claude
committed
2133941