Integer arithmetic on an unknown stays folded when a step is computed (Symbolic.v).

A pointer is its two fields.

Rewrite in E every alignment test of an address the context proves 8-aligned to its answer, before drop_wraps would turn the remainder into an unknown.

Rewrite in E the facts about memory and the module a step reads besides Symbolic.v's: a node's next slot, as bytes and as aux, a function found by name, a callee's frame, and a pointer rebuilt from its fields.

Compute E, an equation r = step g c, as Symbolic.v's compute_step does, with stores and aux kept folded, offsets of 0 dropped, and the facts above.

The function sum.

Every point of sum, numbered: the entry start (0, 1); the loop's head L3, entered from start or from the body (2, 3), before its two instructions and its branch (4 to 6); the body L4, entered (7), then before each of its six instructions and its jump back, which polls (8 to 14); and the exit L5 (15, 16).

At the loop's head, after its first j instructions: the list from pr.1, the sum pr.2 an integer, the walked nodes in htrue, and the frame F; then v7, the list's address, and v8, whether it is not null.

In the body, after its first j instructions: the node at a, its value v and next pointer next, the rest xs; then the pointer v11 to the value and its checked proof chk0, the value v12, the new sum v13, the half-checked node pointer chk1, and the next pointer v15.

What holds at point k of sum_points with the frame F: at the entry, the precondition, the list from the parameter v0 and F; on the edge back, the loop's state in v15 and v13; at the head, sum_head; in the body, sum_body; at the exit, the postcondition, the sum an integer, and htrue and F.

A configuration running sum with the frame F and the callers callers below it: at point k, with no locals and no doom, where the assertion of k holds.

A list's address is 0 or inside the address space.

What a node of the list at a gives the steps that read it.

Add to the context what the separation-logic facts H give a step: a list's address range, and a node's region and next slot.

The point of the next configuration is point n of sum_points or a later one.

Turn the separation-logic hypotheses into what the next point's assertion needs: htrue added at the loop's entry; the list dropped into it at the exit; at a nonnull list, its first node, its pointer taken apart; after the body, the walked node dropped.

The next configuration runs sum at its point, with the same callers and frame and the memory unchanged.

One point of sum_step: the point from Hk, the assertion Ha taken apart with what it gives about memory, the step computed, and its result shown safe.

sum's specification, as one step: from any configuration running sum where its assertion holds with the frame F, under any callers, the step returns an integer to the caller with htrue and F holding, or is safe_step into such a configuration with the same callers and frame, the memory unchanged. Any frame: sum never writes, and a frame need survive only safepoints (sum_safepoint).