Fix/heap design - #36

Draft

nils-loose wants to merge 39 commits into

devfrom

fix/heap-design

Commits on Jun 25, 2026

Add multi-level test harness foundation (L0/L1/L2)

nils-loose
and
claude
committed
a7557fa
Fan out heap-redesign case matrix (O/V/F at L0/L1)

nils-loose
and
claude
committed
b19df47
Add implementation handoff for the heap redesign

nils-loose
and
claude
committed
95dfaa7
feat(heap): G1 - canonical reference-keyed shadow registry

nils-loose
and
claude
committed
67505c4
feat(heap): G2 - concretize unmodeled value-typed returns (no identity recovery)

nils-loose
and
claude
committed
e84b46e
feat(heap): G_oob - configurable out-of-band change detection at GETVALUE

nils-loose
and
claude
committed
5b35699

Commits on Jun 26, 2026

Commits on Jun 29, 2026

Commits on Jun 30, 2026

feat(heap): G3-B core - exact reference equality via provenance (refEquals -> root)

nils-loose
and
claude
committed
59ed40d
refactor(heap): G3-B2 - delete the superseded reference_semantic_change flag + userDeInterned

nils-loose
and
claude
committed
86fdb06
fix(common): checkClassName no longer rejects L-prefixed class names

nils-loose
and
claude
committed
7bb72f4
refactor(nocache): table-drive the six valueOf rewrites off the Boxed enum

nils-loose
and
claude
committed
5bf958e
feat(skills): add jdk-source skill for fetching JDK method source

nils-loose
and
claude
committed
3ac8f10
feat(heap): G4 - extend pure-function UF modeling to primitive returns

nils-loose
and
claude
committed
24118fe
feat(heap): G4 - broaden the pure-function whitelist via the java.lang audit

nils-loose
and
claude
committed
050310b

Commits on Jul 1, 2026

refactor(heap): remove unused shadow-registry inspection accessors

nils-loose
and
claude
committed
8519253
test(heap): remove @See doc-link annotations

nils-loose
and
claude
committed
cd45979
docs(heap): consolidate heap tracking into a single reference

nils-loose
and
claude
committed
b62bb5e
style(heap): drop internal phase/case jargon from comments and Javadoc

nils-loose
and
claude
committed
dc51012
test(heap): describe cases in plain language; drop internal case IDs

nils-loose
and
claude
committed
27d3639
docs(heap): remove superseded design docs; de-jargon reference docs

nils-loose
and
claude
committed
cddfa28
docs(heap): correct reference-equality description in heap-tracking.md

nils-loose
and
claude
committed
710f08d
feat(heap): recover immutable value-typed returns from unmodeled containers

nils-loose
and
claude
committed
d917996
docs(heap): document value-typed container recovery in the reference

nils-loose
and
claude
committed
fb577d5
fix(explorer): downgrade to UNKNOWN when a diverged branch is left unverified

nils-loose
and
claude
committed
afaa656

Commits on Jul 2, 2026

feat(explorer): re-open diverged branches with a bounded attempt count

nils-loose
and
claude
committed
b6309d3
feat(uf): record observed input->output pairs for all return sorts and inject them

nils-loose
and
claude
committed
d6fd4e6
docs(skill): add svcomp-run skill for the SV-COMP harness

nils-loose
and
claude
committed
4f6e42e
chore(svcomp): cap the local runner at 120s per testcase

nils-loose
and
claude
committed
d6cc182

Commits on Jul 6, 2026

fix(uf): pin observed FP outputs with structural = instead of fp.eq

nils-loose
and
claude
committed
e1110cb
fix(soundness): record context loss when an unmodeled callee throws on symbolic input

nils-loose
and
claude
committed
3f16ac6
fix(uf): derive generic-UF sorts from the descriptor; cover INVOKEDYNAMIC throws

nils-loose
and
claude
committed
0968c16
fix(explorer): endpoint-safe UF-pair injection; UNKNOWN must block a SAFE verdict

nils-loose
and
claude
committed
5200688
test: repoint the vacuous substring UF spec at repeat; pin NaN pairs and sort fallback

nils-loose
and
claude
committed
47e564c
docs: reconcile the design reference, test architecture and skills with the as-built code

nils-loose
and
claude
committed
5e06718