diff options
| author |  zinc <zinc@downsta.ir>
| 2026-10-15 05:23:36 +0330 |
|---|---|---|
| committer | zinc <zinc@downsta.ir>
| 2026-10-15 05:23:36 +0330 |
| commit | fe43cc41876ffdb3e714de8efc8a2907d456b5db (patch) | |
| tree | acb86b8b5c46a6ce77a43d3be3a6aa9c8a41abb6 /Makefile | |
| parent | wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, aff... (diff) | |
prover: len/cross-array/fixed-new/affine proofs; keep facts past call loops
Rebased the prover WIP onto main. lafact_keep restores undirtied allocation
facts even when the loop body might free (so a later touch() no longer drops
every length fact). proven_p uses ptr_still so an outer call keeps the check.
entry_fact still supplies the size for the "might free" explain reason.
bounds_prover.zc and explain_prover.zc land with test.sh coverage.
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions