Repository navigation

Support splitting packed DSTs through unaligned element views - #3750

Closed

joshlf wants to merge 12 commits into

Guzdt7nfgmmi7y3e4taezg43ssexn4hrffrom

Gcf7sazu56b7hwm5kb56l7lndntqb7aw2

Closed

Support splitting packed DSTs through unaligned element views#3750
joshlf wants to merge 12 commits into
Guzdt7nfgmmi7y3e4taezg43ssexn4hrffrom
Gcf7sazu56b7hwm5kb56l7lndntqb7aw2

Commits on Oct 5, 2026
- Check native total and partial Aeneas specifications
  joshlf
  committed
  5a84ff2
- Strengthen arithmetic specifications and prove arithmetic corollaries
  joshlf
  committed
  bc7fdcc
- Reuse Aeneas specifications for views and indexed loops
  joshlf
  committed
  345e102
- Prove trailing-layout normalization and capacity arithmetic
  joshlf
  committed
  a3a994c
- Refine recursive record semantics into normalized layouts
  joshlf
  committed
  5bc26a2
- Model alignment and phase encoding as a bounded mathematical pair
  joshlf
  committed
  371fbd1
- Preserve nested DST padding throughout runtime layout operations
  joshlf
  committed
  a71947f
- Compare nested DST sizes with a recursive Rust oracle
  joshlf
  committed
  ef2804b
- Support splitting packed DSTs through unaligned element views
  joshlf
  committed
  381343b
- Move pointer cast implementation into its own source file
  joshlf
  committed
  7c15a27
- Separate numerical cast planning from typed pointer projection
  joshlf
  committed
  44c82ce
- Verify doc-owned specifications over recursive mathematical models
  joshlf
  committed
  e7c8ab5