Strings the world lends, in the program logic of Logic.v (docs/logic.md). setlocale(k, NULL) returns libc's own name for the locale category k: memory the program does not own and may read only while the world keeps it. A weakest precondition cannot remember across steps which string a query returned, since the memory and the world are the state, not the assertion. A ghost piece does (PName of Pieces.v): lent k p t says the world lends the string t at p under the key k, and the world interpretation wi ties every such piece to the world.

What a proof needs of wi is one fact, lent_at: a lent string is a C string (c_string), in an object at a multiple of 8, and apart from every object owning a piece of memory in the ghost heap. Its triples are generic in wi under that hypothesis:

• wp_lent_query: a call that returns the lent pointer and changes nothing, such as setlocale's query;
• wp_strlen_lent: strlen of a lent string;
• wp_memcpy_lent: memcpy of a prefix of a lent string, with its NUL, into an owned block, whose aux slots afterwards are what the copy left there (slots_after).

The token is persistent: a lent string is read, never given back, so no triple changes a lent string. Before it is lent, a name is owned whole (named), and a setter that changes it, such as setlocale(LC_ALL, ""), takes it:

• wp_lend: a call that renames the keys whose names it is given, and lends the new names. The ghost heap renames them (rename_update); what the call must keep of the state is its premise, for the contract and wi to discharge.