rocq/glibc/LenLogic.v
rocq/glibc/len.c, linked with nanofil's IR of user glibc's string/strlen.c, through the program logic of Logic.v (docs/glibc-ir.md).
main returns strlen(msg) for the 13-byte literal "hello, glibc". No contract describes strlen here: the linked module defines __strlen, glibc's word-at-a-time scan, and the weak alias strlen that names it, so the call is an ordinary direct call (wp_call_bind) and the proof walks glibc's own IR. The module calls nothing outside itself; the registry is empty.
The call is taken by StrlenLogic.v's wp_glibc_strlen, the triple of glibc's strlen for any string: the literal's object is 8-aligned and 16 bytes, its 13 bytes rounded up to whole words (Run.v's layout; filcc's literal object is also 16 bytes, probed in docs/glibc-ir.md), and the program owns its life and both words (msg_ps), which is the triple's precondition. Its first zero is 12 bytes in, so strlen returns 12.
len_never_panics is never_panics for main, through GlibcLogic.v's pieces_never_panics: Iris adequacy where the program starts owning pieces of its initial memory, here the literal's.
The module
The fixture decodes to len_module.
Proof 2 steps Qed
The address of the literal msg, renamed len#msg by link.pl.
The literal's capability, read-only.
The literal's region: its 13 bytes rounded up to 16.
The module's symbols: strlen is __strlen's address.
The module's initial memory.
Laying out the module gives len_globals and len_mem.
Proof 3 steps Qed
The function named n of the module, or an empty one.
len.c's main.
glibc's __strlen.
The literal's pieces
The literal's first word, "hello, g", little-endian.
Its second word, "libc" and the NUL, then the three zero bytes the layout's rounding adds.
The pieces the program owns: the literal's life and its two words.
The pieces' keys are distinct.
Proof 3 steps Qed
The literal's object is registered with its region.
Proof 2 steps Qed
The initial memory holds the literal as msg_ps says.
Proof 5 steps Qed
The initial memory's one live object is apart from itself.
Proof 8 steps Qed
Over any runtime
The proof over the runtime R.
The linked genv, whose free is R's.
The expressions of its language.
A call of strlen runs __strlen, through the alias.
Proof 2 steps Qed
main is a function of the module.
Proof 2 steps Qed
The Iris instance of the module: no contracts, no world.
glibc's strlen, called with the literal, owning its pieces: wp_glibc_strlen with its two words, returning 12 and handing the pieces back.
Proof 30 steps Qed
main, owning the literal, returns 12: glibc's strlen of it.
Proof 12 steps Qed
len.c linked with glibc's strlen never panics: called with any arguments, with any fuel and whatever the runtime does at its safepoints, no state of its run fails. By pieces_never_panics from main_spec, the program owning the literal's pieces.
Proof 12 steps Qed
The theorem for the interpreter's runtime.
len.c with glibc's strlen never panics under the interpreter's runtime.