rocq/glibc/StrlenLogic.v
A triple for glibc's own __strlen, as nanofil compiles user glibc's string/strlen.c (docs/glibc-ir.md): for any string, not one literal, over any registry and world, so a program linked with glibc's strlen uses it as a rule at its call.
glibc's strlen reads whole aligned 8-byte words: first the word holding the string's first byte, its bytes before the string masked off by a shift, then each next word until one holds a zero byte (StrlenBits.v). Every word it reads is a whole word of the string's object, so the triple's precondition is about words, not bytes:
- the capability names the object b, read-write or read-only, and b is 8-aligned;
- the caller owns the life of b and the words ws from the word that holds the first byte, through the word that holds the NUL, every byte of each, including bytes past the NUL (
words_ps); - those words lie inside b's region.
This is the whole-word rounding glibc's strlen depends on. A string whose NUL is the last byte of an object that ends mid-word does not meet it, and on such an object glibc's strlen would read past the end. Fil-C rounds every object up to a whole word, as filcc gives a 13-byte literal a 16-byte object, and the model's layout rounds data to 8 (docs/glibc-ir.md, Findings). The result is the index of the first zero byte from the string's start (first_zero).
loop_spec is the loop block, for any number of words, by induction on them; wp_glibc_strlen is the entry block, whose NUL is in the first word or the loop finds it.
glibc's __strlen, as the linked fixture of len.c holds it.
The pieces of the 64-bit words ws from offset o of the object b.
The bytes of the words ws, little-endian, in order.
The first zero of the bytes bs is at n.
The bytes of the words w :: ws are w's eight, then ws's.
Proof 1 step Qed
Byte i below 8 of w :: ws is w's byte i.
Proof 4 steps Qed
Byte 8 + i of w :: ws is byte i of ws.
Proof 5 steps Qed
Where the first zero of the bytes of w :: ws from k, k below 8, is at n, and k + n is inside w: byte k + n of w is zero and its bytes from k before it are not.
Proof 9 steps Qed
Where the first zero of the bytes of w :: ws from k is at n, and k + n is past w: w's bytes from k are nonzero, and the first zero of ws's bytes is at k + n - 8.
Proof 19 steps Qed
A temporary's value at class k is what the environment holds for it, taken at k.
Proof 4 steps Qed
The triple over the runtime R and the Logic instance LG0.
The Iris instance of the registry and wi.
The expressions of the language.
One step whose premises reduce: a pure let, a flight, entering a block, or a goto. The values stay symbolic.
Drop each wrap to 64 or 32 bits that arithmetic shows the identity.
Keep only arithmetic hypotheses, so lia does not read the rest.
Compute each closed shift factor 2 ^ (n mod m).
An address or integer fact, by arithmetic.
A branch whose condition is closed: computed.
The v4 lookup through the puts of a block, to the frame's e.
Name the integer the temporary name holds v, by computation or arithmetic.
Name the address of the pointer the temporary name holds v.
The loop's block, L28: load the next word and test it for a zero.
The loop, entered with pr.1 the previous word's pointer q and v4 the string's address a, owning the words ws from offset o of the 8-aligned word b + o on, whose first zero byte is t bytes in: strlen returns b + o + t - a, the pieces handed back.
Proof 108 steps Qed
w holds the NUL, at byte t.
w has no zero byte: the next word.
glibc's strlen of p: owning the life of the 8-aligned object b and the words ws of it from the word that holds p's byte, inside its region, whose first zero byte from p is n bytes in, the call returns n and hands the pieces back.
Proof 117 steps Qed
The NUL is in the first word.
The NUL is in a later word: the loop.