rocq/glibc/SayLogic.v
rocq/glibc/say.c, linked with nanofil's IR of user glibc's string/strlen.c and io/write.c, through the program logic of Logic.v (docs/glibc-ir.md).
main writes the literal "hello, glibc\n" to descriptor 1 with write(1, msg, strlen(msg)). Both calls run glibc's own IR: strlen is __strlen's word-at-a-time scan, taken by StrlenLogic.v's triple wp_glibc_strlen, and write is the alias of __libc_write, whose body calls libpizlo's zsys_write and returns what it returns. The linked module defines everything but zsys_write, so that one name is the registry's, with the trusted contract of ZsysWrite.v; the rest is proved.
The world is ZsysWrite.v's fd_world, interpreted by fd_wi for descriptor 1: errno a writable int apart from the literal, and descriptor 1 not libpizlo's log. ZsysWrite.v names what the world is trusted to be: the thread's own allocated errno, glibc's errno handler registered, no errno logging. say_logic_safe is the labelled machine's safety of main from any such memory and world holding the literal, with the result 0.
The module
The fixture decodes to say_module.
Proof 2 steps Qed
The address of the literal msg, renamed say#msg by link.pl.
The literal's capability, read-only.
The literal's region: its 14 bytes rounded up to 16.
The module's symbols, as laying it out places them.
Laying out the module gives say_globals.
Proof 2 steps Qed
The function named n of the module, or an empty one.
say.c's main.
glibc's __strlen.
glibc's __libc_write.
The literal's pieces
The literal's first word, "hello, g", little-endian.
Its second word, "libc\n" and the NUL, then the two 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
Every piece is of the literal's object.
Proof 4 steps Qed
Where the pieces agree, the literal's 13 bytes are readable through its capability: what zsys_write's precondition asks of the buffer.
Proof 29 steps Qed
The contracts
The registry: zsys_write's contract alone; everything else the program calls is in the module.
main called with no arguments.
Over any runtime
The proof over the runtime R.
The linked genv: the module, its symbols, R's free.
A call of strlen runs __strlen.
Proof 2 steps Qed
A call of write runs __libc_write.
Proof 2 steps Qed
The Iris instance of say.c: zsys_write's contract and fd_wi for descriptor 1.
The expressions of say.c's language.
glibc's strlen, called with the literal, owning its pieces: wp_glibc_strlen with its two words, returning 13.
Proof 30 steps Qed
main, owning the literal, returns 0: glibc's strlen measures it, glibc's write hands it to zsys_write for descriptor 1, whatever that returns, and the pieces are still owned.
Proof 24 steps Qed
main is safe: from a ready runtime, live objects apart, a memory holding the literal as msg_ps says, and a world whose errno is a writable int outside the literal's object and whose log descriptor, if any, is not 1, with any fuel, no labelled run stops with a failure_ending, and a run that returns returns 0. By heap_labelled_safe from main_spec, the ghost heap starting with the literal's pieces.
Proof 22 steps Qed
The theorem for the interpreter's runtime.