Function pointers: ghost arguments, correct witness arity, and array-length refinements - #281

Closed

hei411 wants to merge 11 commits into

mainfrom

heili/ghost-fnptr

Commits on Aug 28, 2026

Add a failing test for _ghost_arg on function pointers

hei411
and
Copilot
committed
f52988a
Support _ghost_arg on function pointers

hei411
and
Copilot
committed
2263cd3
Tidy up ghost-fnptr: fix check.rs gap, trim test

hei411
and
Copilot
committed
ed69d54
Revert fnptr ghost-arg plumbing; add eta rules and a witness-shape test

hei411
and
Copilot
committed
622a0ae
Infer the function-pointer witness: make `c` the pair `(ELIMS & GHOSTS)`

hei411
and
Copilot
committed
e6861a0
Cover differing ghost arities in the across-shapes fnptr test

hei411
and
Copilot
committed
0febcbb
Revert emit.rs to main; keep the eta rules and the ghost_fnptr test

hei411
and
Copilot
committed
18ef155
Re-do the fnptr witness without the deref lookup table

hei411
and
Copilot
committed
a99094f
Test fnptr witnesses for structs with a `__spec` companion

hei411
and
Copilot
committed
f9940f4
test: red repro for `_array` `_length` refine + function pointer

hei411
and
Copilot
committed
1a1888d
Emit an array field's `_length` as a spec projection, not `length_of`

hei411
and
Copilot
committed
97ecc1c