Update `llzk-pod-to-scalar` to split pods within arrays to multiple arrays - #565

Merged

tim-hoffman merged 150 commits into

mainfrom

th/make_pod_to_scalar_split_arrays

Jul 28, 2026

Commits on Jun 18, 2026

changelog
tim-hoffman
committed
d659eaf
add test case
tim-hoffman
committed
d256d32
split pods within arrays to multiple arrays
tim-hoffman
committed
f6e898e
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
committed
cdf8853
fix compile error from merge
tim-hoffman
committed
6793d6e
fix shadowing warnings
tim-hoffman
committed
477c532
reverse pipeline ordering based on this update
tim-hoffman
committed
3d01279

Commits on Jun 22, 2026

Commits on Jun 23, 2026

fix: Avoid assuming one backing array for `array.len`
tim-hoffman
committed
3166d45
fix: Populate result split sizes before cloning attrs
tim-hoffman
committed
2d0db69
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
committed
233a887
fix: split equality constraints over POD arrays
tim-hoffman
committed
e516171
fix: Avoid creating arrays whose elements are arrays
tim-hoffman
committed
c5d0d62
fix dangling ref
tim-hoffman
committed
34bd6e0
additional regression test
tim-hoffman
committed
4563267
clang-tidy cleanup
tim-hoffman
committed
fae7959

Commits on Jun 24, 2026

Commits on Jul 1, 2026

Commits on Jul 2, 2026

fix: Handle uninitialized deferred POD-array reads
tim-hoffman
committed
e8bceaa
fix: Apply uninitialized fallback to static POD arrays
tim-hoffman
committed
0b804d4
fix: Avoid aborting on dynamic nested POD operands
tim-hoffman
committed
3d0e443
fix: Split pod.read-backed array returns
tim-hoffman
committed
9956341
fix: Rewrite quantifiers over POD arrays
tim-hoffman
committed
ce0ce8f
clang-tidy
tim-hoffman
committed
ac379dd
fix: Honor writes before resolving virtual POD reads
tim-hoffman
committed
3b352b3
fix: Split unifiable casts for POD arrays
tim-hoffman
committed
8ea12b1
fix: Split POD-array call operands from POD reads
tim-hoffman
committed
ddc518b
fix: Preserve member read offsets when splitting POD arrays
tim-hoffman
committed
1401bf2
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
authored
4021ad1
fix: Preserve the source shape for affine empty-POD arrays
tim-hoffman
committed
74d0b45
fix: Use a writable affine-aware array for static POD-array leaves
tim-hoffman
committed
bd186a3
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
committed
21f2e6d

Commits on Jul 3, 2026

Commits on Jul 6, 2026

IR: allow `none` as array element type
tim-hoffman
committed
34d5766
fix: Keep dynamic split-array shapes tied together
tim-hoffman
committed
09f0453
fix: Avoid treating loop-carried writes as unwritten
tim-hoffman
committed
2bfadea
fix: Preserve source shape carrier on POD-array extracts
tim-hoffman
committed
879fa94
fix: handle `NoneType` in `computeEmitEqCardinality()`
tim-hoffman
committed
4f7b346
fix: Preserve member array shape when reading split POD arrays
tim-hoffman
committed
2c28973
fix: Rebuild empty-POD quantifier rows as arrays
tim-hoffman
committed
cdf0435
fix: Compare carriers regardless of equality operand order
tim-hoffman
committed
6b072c3
fix: Update shape carriers when inserting POD subarrays
tim-hoffman
committed
a01bdcf
fix: Constrain shapes for empty-POD subarray containment
tim-hoffman
committed
a4738eb

Commits on Jul 7, 2026

fix: Respect dominating POD writes before nested reads
tim-hoffman
committed
4093b97
fix: Materialize affine virtual PODs before late uses
tim-hoffman
committed
6c4552a
fix nullptr failure
tim-hoffman
committed
b0efade
fix: Preserve carriers for nested POD-array shapes
tim-hoffman
committed
2f653cb
fix segfault
tim-hoffman
committed
c57a001
fix: Tie synthesized carriers to affine-shaped arrays
tim-hoffman
committed
090a46e
fix: Compare shapes for non-empty POD containment
tim-hoffman
committed
052252f
fix: Avoid scalarizing shape-only array carriers
tim-hoffman
committed
8f6fe30
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
authored
177e0ac

Commits on Jul 8, 2026

fix: Use the shape-carrier predicate for suffixes
tim-hoffman
committed
ddd0ee3
fix: handle affine array nondets in array-to-scalar
tim-hoffman
committed
41bfb1b
fix: Reserve the shape-carrier key from POD records
tim-hoffman
committed
b193f29
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
authored
ebd60e3
clang-tidy cleanup
tim-hoffman
committed
f5043e6
fix: Preserve POD equality values before later virtual writes
tim-hoffman
committed
9e95d58
fix: Cache the shape carrier with deferred leaf arrays
tim-hoffman
committed
0380feb
fix: Use the carrier for zero-leaf array casts
tim-hoffman
committed
a22f135
fix: Ignore unrelated unrealized casts in residual checks
tim-hoffman
committed
d830407
fix: Deferred pod-array read resolution bails out too early
tim-hoffman
committed
8e1df41
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
authored
7f5234a
fix: Clear partial leaf arrays before fallback
tim-hoffman
committed
ecd253d
fix format
tim-hoffman
committed
dc8fbfc
fix: Don’t forward parent writes into loop reads
tim-hoffman
committed
6321758
fix: Compare empty POD-array shapes by length
tim-hoffman
committed
ffda29a

Commits on Jul 9, 2026

fix: Update destination carriers for static subarray inserts
tim-hoffman
committed
732e73d
fix: Still fold lengths of static shape carriers
tim-hoffman
committed
615e8de
reorg new tests into fewer files
tim-hoffman
committed
c192a09
move tests to proper directory
tim-hoffman
committed
07febf1
fix: Preserve control-flow writes to virtual PODs
tim-hoffman
committed
b5c7678
fix: Preserve affine array shape when all leaves gain rank
tim-hoffman
committed
e4ded04
fix: handle POD equality with type variables
tim-hoffman
committed
55bb114
fix: array shape carrier issues (x3)
tim-hoffman
committed
302b4cd
fix: pod-array constraint issues (x2)
tim-hoffman
committed
c4e3f1d
fix shadowing warnings
tim-hoffman
committed
fa9bdbb
fix: Split nested pre-write equalities before updating virtual PODs
tim-hoffman
committed
6ce091c
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
authored
0411064

Commits on Jul 10, 2026

Commits on Jul 13, 2026

Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
committed
7da8b54
fix some issues that show up post-merge
tim-hoffman
committed
76631bd
remove code duplication
tim-hoffman
committed
67a2a71
refactor step 3 to clean it up a bit
tim-hoffman
committed
e8722c1
fix shadowing warnings
tim-hoffman
committed
5a2db39
fix: Handle generic lhs arrays in POD-array containment
tim-hoffman
committed
2733b60
fix: Populate shape carriers for dynamic quantifier iterands
tim-hoffman
committed
04f30bd

Commits on Jul 14, 2026

add test with member name collision
tim-hoffman
committed
c7f3394
remove useless function
tim-hoffman
committed
7e88387
replace functions with constants
tim-hoffman
committed
48a3e72
remove redundant cast
tim-hoffman
committed
a81ebd1
use type alias more widely
tim-hoffman
committed
fe546cf
assorted minor changes
tim-hoffman
committed
98e7739
document "virtual pod"
tim-hoffman
committed
a844984
move some functions to `RecordChain`
tim-hoffman
committed
1c37e06
add `ArrayType::getSelectionType()` to remove some duplication
tim-hoffman
committed
adb864c
reorg function defs
tim-hoffman
committed
1ea5c95
add `-verify-diagnostics` to more tests just to be safe
tim-hoffman
committed
1466aae

Commits on Jul 15, 2026

update documentation
tim-hoffman
committed
df0e8b9
make array read/write gen helpers reusable
tim-hoffman
committed
2055a67

Commits on Jul 23, 2026

Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
committed
eaf3d53
fix: tvar inference crash from no param templates
tim-hoffman
committed
729635a
Use tvar-inference and quantifier-lowering to simplify
tim-hoffman
committed
5b99ebe
relax allowed replacement type restriction in `llzk-infer-tvar`
tim-hoffman
committed
997a7ed
update test that now passes
tim-hoffman
committed
697b0bd
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
committed
77968a7
remove remaining `unrealized_conversion_cast`
tim-hoffman
committed
0653b16
fix: multiple unifiable_cast to different types
tim-hoffman
committed
5c07dc4
clarify comment
tim-hoffman
committed
119282a

Commits on Jul 24, 2026

Commits on Jul 25, 2026

Commits on Jul 27, 2026

Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
committed
abf44e2
fix: Strip signal metadata from nested shape carriers
tim-hoffman
committed
179814b
fix: Reject containment on ragged nested leaves
tim-hoffman
committed
af9588a
fix: avoid ragged-shape provenance across SSA boundaries for now
tim-hoffman
committed
fbd21d8
fix: remove fixed iteration because it's monotonic
tim-hoffman
committed
a68fd16
fix: ragged array issues
tim-hoffman
committed
0bdc6d8
fix: Keep shape carriers column-addressable
tim-hoffman
committed
209ba20
fix: Preserve attributes on rewritten array-of-POD calls
tim-hoffman
committed
292487f
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
authored
4df3245
fix: preserve attributes
tim-hoffman
committed
73ca3c5
fixup
tim-hoffman
committed
05e03c0
cleanup duplicate code
tim-hoffman
committed
5266e85
Merge branch 'main' into th/make_pod_to_scalar_split_arrays
tim-hoffman
authored
52f3cae