aboutsummaryrefslogtreecommitdiff
path: root/tests/programs/bounds_prover.expected
Commit message (Collapse)AuthorAgeFilesLines
* prover: len/cross-array/fixed-new/affine proofs; keep facts past call loopsGravatar zinc 13 days1-0/+4
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.