Issue #641: Result summaries reach fewer bodies than ADR-359 D1 says: any loop, assignment, match or lambda stops them

Open and answer this issue on GitHub.

ready · opened 2026-10-17 · updated 2026-10-17 · 0 comments

How it came up

The agent that built ADR-359 D1-D3 (767cfc1, 0.0.997, #632) gave a result summary only to free functions whose body consists solely of let, return and if. A body with any of the following gets none, even where it does not touch the result:

• a loop;
• an assignment;
• a match;
• a block or lambda inside an expression.

D1 says more. A function gets a summary when every exit returns a whole number the prover reads, there is no loop that changes a name it reads, there is no match, and no call on the way can come back to it.

The build is therefore stricter than the text. It proves less than the specification promises, and never anything false. The owner decided (round on #632) to keep D1’s text as it is and record the gap here rather than narrow the specification.

To build

1. Loops and assignments that the result does not read. A loop or an assignment that changes no name an exit’s value or path reads does not stop the summary. Tests:
   • a function with a logging loop over an unrelated counter still answers example(2) - 1 == 11;
   • a function where the loop changes a name the result reads still has no summary.
2. Lambdas and blocks inside an expression that the result does not read do not stop it.
3. Methods, not only free functions, where D1’s conditions hold. A method that reads self’s fields reads them as parameters.
4. Loops that the result does read. Once #640 (ADR-361) carries a claim through a loop, a loop whose invariant gives the exit’s value may enter the summary. This is a decision for later; ADR-359 says “loops and recursion in a summary” is not decided. Do not build it here.
5. Re-run the NIKAIA_PROVER_COUNTS=1 counters and callgrind over lower-std (limit: ADR-359 D10’s +5 %). Check every new refutation by hand (D9).

Back to Open Issues