moon/zygotec/tests/programs/explain_prover.zc, branch main work-in-progress programming language.
https://git.downsta.ir/moon/zygotec/atom?h=main2026-10-15T01:55:58+00:00prover: do not restore length facts after a call-loop2026-10-15T01:55:58+00:00zinczinc@downsta.ir2026-10-15T01:55:58+00:00urn:sha1:a6e52065bb7eaee3bbef5a1c3f879c616e3d24bc
Restoring undirtied lafacts when the body might free was wrong: push can
grow an array without dirtying its name, so a[99] after push warned against
a stale length 0. Keep the old lafact_keep rule; reorder explain_prover so
the constant/affine cases run before the touch() loops.
wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, affine i*n+k); unbuilt and untested2026-10-15T01:47:02+00:00zinczinc@downsta.ir2026-10-14T17:16:17+00:00urn:sha1:a1d546cc74a72abc4973bf96f72bbd529320d711