[SwayamInSync]

A loop that fills a local array could not be verified. On the base (#73):

int filled()
  cv::post(cv::result == 0)
{
  int a[4];
  for (int i = 0; i < 4; i = i + 1)
    cv::invariant(0 <= i && i <= 4)
    cv::invariant(cv::forall(k, 0, i, a[k] == 0))
    cv::decreases(4 - i)
  {
    a[i] = 0;
  }
  return a[3];
}

filled.cpp:7:19: error: verification failed: filled [...::initialization@7:19#2] (counterexample: ...) [backend=z3] [reason=counterexample]

Now:

Verified: filled [backend=z3]

Stacked on #73. Found while starting B3-2 (constructors), whose bodies initialize storage in loops.

Causes

1. The head kept the initialization of the state before the loop. A store through local or dynamic storage sets its cell's initialization bit, but the loop's modified set (collectModified) named only the value heap for a store, so the head's initialization heap was the one before the loop: every iteration after the first saw what the earlier ones wrote as uninitialized, and after the loop only the state before it remained.
2. The head assumed an invariant without its definedness. Entry, the end of an iteration, and every continue assert each invariant's definedness (its core checks and the memory checks recorded for it) before the invariant; the head assumed only the invariant. So nothing at the head said that a[k] for k < i was initialized, which C++ contracts cannot state.

Fixing (2) alone made filled verify vacuously: the assumed initialization contradicted the stale heap of (1), forcing i == 0 at the head. (1) is what makes (2) hold in the model.

Design

• Initialization across a loop. A store through a pointer with a lifetime identity modifies the initialization heap, so the head gets a fresh version. No lifetime begins or ends in a loop (the converter rejects addressable declarations, allocation, and deallocation there), so a loop only initializes storage: the head assumes forall a. init_before[a] -> init_head[a], triggered by reads of the head's version (initializationKept). startsLifetime withholds it from a loop that starts a lifetime, which none can today, so that admitting one later cannot make the assumption false. No frame bounds the rest: no claim needs a cell to be uninitialized, so taking more cells as possibly initialized loses nothing.
• Definedness at the head. Each invariant's definedness, the checks exprSafetyChecks collects (shared with emitExprSafety, which asserts them), is assumed at the head before the invariant: every path into the head asserts both, so both hold there by the same induction.
• Which checks. A check is assumed when the condition it asks for, without its guards (checkedCondition: !g || c, a quantified check's body), reads state the loop modifies (readsLoopState: a variable or field it assigns, a load or a heap-reading spec when it writes memory, validity or initialization when it changes those). A condition of nothing the loop changes holds at the head as it held before the loop; when it is false, the invariant's definedness would only constrain its guards, which the invariant can state. Assuming every check made the ULEB128 case study's encode_uleb128 4.7 times larger after simplification (1.79 to 8.45 million nodes) and its Lean export exceed its budget: its invariants count <= k || buffer[k] == uleb_byte_machine(original, k) carry the helper's definedness at a constant index under a guard of count. With the rule it is 1.83 million nodes, and the export is 20.1 MB against 19.9 MB on the base.
• References. Dafny checks an invariant's well-formedness once, in the loop's arbitrary state, from the invariants before it (TrLoop: if (!w) { CheckWellformed(inv); assume inv; ... assume false }), and assumes its CanCallAssumption at the head. That self-framing rule works where storage is always initialized; C++ storage is not, and its initialization is not expressible in a contract (Frama-C asks for \initialized). Here definedness is proved where the invariant is, inductively, and holds at the head with it.

Tests

suite/loop_initialization.cpp (Z3, with a check that no proof is vacuous, and BMC):

• filled: the loop above;
• incremented: a loop reads elements a loop before it initialized, which no invariant of its own states (the kept initialization);
• kept: a scalar initialized before a loop that writes an array stays initialized;
• partially_filled: an element the loop never writes is not initialized after it (initialization);
• read_first: nor one it reads before writing (initialization);
• last: an invariant reading p[i] bounds i at the head, so return p[i] is in bounds;
• log2_floor: a shift in an invariant bounds its amount at the head, so the condition's shift is defined;
• overrun: an invariant reading c[i] past the end still fails where it is preserved.

Mutants, each built on an assertions build and run on loop_initialization.cpp, out_parameters.cpp, loop_frames.cpp, old_loop_invariant_definedness_fail.cpp, and shared_logic_terms.test: 7 of 7 killed.

Mutant	Killed by
no definedness at the head (the base's rule)	loop_initialization (filled, incremented, last, log2_floor)
a store to local storage leaves the initialization heap alone (the base's rule)	loop_initialization (partially_filled; filled verifies vacuously)
initialization not kept across the head	loop_initialization (incremented)
only the core checks assumed	loop_initialization (last)
only the memory checks assumed	loop_initialization (log2_floor)
initialization not counted as loop state	loop_initialization
the guards decide whether a check reads loop state	shared_logic_terms (the Lean export exceeds its budget)

On the base, filled, incremented, last, and log2_floor fail (initialization, overflow, shift), and partially_filled fails at its invariant's preservation instead of at the read after the loop.

startsLifetime cannot be exercised: the converter rejects every construct that starts a lifetime in a loop. It keeps the kept-initialization fact from becoming false if one is admitted.

Docs

• functions-loops.rst: an invariant holds with its definedness, initialization across loops, a checked example (filled, partially_filled).
• Release notes: "Loops that initialize local storage".
• DESIGN.md: loop contracts. ARCHITECTURE.md: the loop rule with definedness, initialization at the head.

Found alongside

• A loop that stores to local storage havocs the whole value heap: the region of a store whose root is local storage is unknown to loopWriteRegions, and the function's own frame is not used when the function owns storage. That is sound, but the loop forgets the values of every other object (kept with a postcondition on x's value fails). Next PR.

Checked

• The Verify suite on a release build: 459 passed (the exhaustive decoder filtered out), 1221 s with 40 workers. A first run, before the rule on which checks, failed shared_logic_terms.test (the export above) and counterexample_confirmation.cpp (which certifier application a message names, under load; it passes alone and has no loops).
• The doc pages' examples (functions-loops, DESIGN): 32 checked, 0 failed; docs_examples.test and docs_coverage.test pass.
• llvm_uleb128.cpp's Lean export: 20.1 MB (19.9 MB on the base); encode_uleb128's module 1.83 million nodes after simplification (1.79 million).