moon/zygotec/tests/programs/bounds_prover.expected, branch work/uninit-locals work-in-progress programming language.
https://git.downsta.ir/moon/zygotec/atom?h=work%2Funinit-locals2026-10-15T01:53:36+00:00prover: len/cross-array/fixed-new/affine proofs; keep facts past call loops2026-10-15T01:53:36+00:00zinczinc@downsta.ir2026-10-15T01:53:36+00:00urn:sha1:fe43cc41876ffdb3e714de8efc8a2907d456b5db
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.