rocq/glibc/GlibcLogic.v

What the proofs of programs linked with user glibc's IR share (docs/glibc-ir.md): a raw load through a read-only capability, Iris adequacy for a program that starts owning pieces of its initial memory, and tactics that take a step whose values are all known by computing it.

glibc's functions are module code here, so their runs are walked with Logic.v's rules like the program's own. When the program's data is fixed, as a literal is, every value of such a run is a numeral: step takes the next instruction by its rule, every premise computed by the virtual machine, and norm_env keeps the frame's environment a list of numerals, so values do not grow into the expressions that made them.

From iris.proofmode Require Import proofmode

From iris.base_logic.lib Require Import gen_heap

From iris.program_logic Require Import language weakestpre

From Stdlib Require Import String ZArith Lia

From Nanofil Require Import Term Syntax Values Memory Runtime Ops Semantics Run Machine Panics StepRules ExternalCalls ExternalMachine Pieces Heap Language Logic

Open Scope Z_scope

Open Scope list_scope

Over a Logic instance

The shared rules and tactics over the runtime R and the Logic instance LG.

27Module GlibcLogicOn R : Runtime LG₀ : LogicSigR

28Module LG ≔ LG0

29Module L ≔ LG.L

30Module P ≔ LG.P

Import L LG

Tactics

An equation whose right side may be unknown: the left side computed, the right side made it, and the two checked by the virtual machine, so the kernel checks it the same way.

38Ltac vm_eq ≔

match goal with|- ?l = ?r⇒let v ≔ eval vm_compute in l in unify r vend;vm_compute;reflexivity

A pure premise of a step, all of whose values are known: by computation.

44Ltac side ≔

lazymatch goal with|- ∀_ : mem, _⇒intros ? ; vm_eq|- ptr_cap_ = _ ∨ ptr_cap_ = _⇒right ; reflexivity|- _ ≤ _⇒vm_compute ; congruence|- _ = _⇒vm_eqend

Replace the environment e of the goal by e', which the virtual machine shows equal.

54Ltac replace_env e e′ ≔

assert Henv : e = e′ by vm_compute ; reflexivity ; try rewrite Henv ; clear Henv

Compute the environment of the goal's frame to a list of numerals.

58Ltac norm_env ≔

match goal with|- context [mkFrame?f ?e ?ls ?d ?pt]⇒let e′ ≔ eval vm_compute in e in replace_env e e′end

One step of a block by its rule, or fail: a pure let, a flight, a branch, a goto, or entering a block, whose instructions are then unfolded.

66Ltac step ≔

74Section rules

75Context `{!invGS_genhlc Σ, !gen_heapGSpiece pval Σ}

76Context world : Type registry : name → optioncontractworld wi : mem → world → gmappiece pval → Prop `{!SafepointStablewi} ge : genv

The Iris instance of the registry and wi.

80Instance rules_irisGS: irisGS_genhlc nanofil_langregistry ge Σ ≔

nanofil_irisGSregistry wi ge

The expressions of the language.

83Notation gexpr ≔ language.exprnanofil_langregistry ge

wp_raw_load through a read-write or read-only capability: a raw load of a long at offset off from the proven pointer p, which addresses offset o of the live object b, where the cell holds v: d is bound to v modulo 2^64. glibc's strlen reads a string literal's words through its read-only capability.

90Lemma wp_raw_load_read

∀ f e ls l d k off args rest j classes p b reg o v Φ

op_arg_classesRawLoadLdL off k = Someclasses

map2_optionvalue_xge e classes args = SomeWPtrp

ptr_capp = Objb ∨ ptr_capp = Rob

raw_addressptr_addrp off = b + o

liveb reg −∗ icellb o v −∗ ▷liveb reg −∗ icellb o v −∗ WPERunmkFramef putd WIntv mod 2 ^ 64 e ls None Execl rest j : gexpr {Φ} −∗ WPERunmkFramef e ls None Execl Letd k RawLoadLdL off args :: rest j : gexpr {Φ}

Proof 20 steps Qed

intros Hc Hx Hp Ha

iIntros Hl Hc HK

iApply wp_readregistry wi ge PLiveb, VLivereg ++ cellb o v _ _ [ ] with [Hl Hc] [HK]

–intros m fuel Hf & _

apply all_agree_app in Hf as Hlv _ Hcl

cbn [ agree_piece fst snd ] in Hlv

destruct cell_bounds_ _ _ _ _ Hlv Hcl as Ho He

apply rule_let with classes := classes xs := WPtrp ; reflexivity | exact Hc | exact Hx |

rewrite op_raw_loadm k p off

+rewrite Ha cell_loadm b reg o v b + o Hlv Hcl eq_refl

reflexivity

+rewrite Ha

apply access_read_ b reg ; exact Hp | exact proj1Hlv | lia | lia | apply Z.mod_1_r

–rewrite pts_app

iFrame

–iNext

iIntros H

rewrite pts_app

iDestruct H as [Hl Hc]

iApply HK with Hl Hc

Iris adequacy where the program starts owning the pieces ps of its initial memory, distinct and agreeing with it: if, for every admissible input, owning ps gives the entry's frame a weakest precondition with no contracts under any invariant and ghost heap instance, the module never panics. heap_never_panics with ps for its empty ghost heap.

119Theorem pieces_never_panics

∀ Σ HinvP : invGpreSΣ HheapP : gen_heapGpreSpiece pval Σ md entry input : listword → Prop globals m f ps : listpiece × pval

initial_memorymd = Someglobals, m

find_fnP.program_genvmd globals entry = SomeDefinedf

live_disjointm

all_agreem ps

NoDupps.*1

∀xs, inputxs → ∃fr, call_framef xs = Somefr ∧ ∀HinvG : invGS_genHasNoLc Σ HheapG : gen_heapGSpiece pval Σ, ptsps ⊢ WPERunfr : language.exprnanofil_langno_contracts P.program_genvmd globals {_. True}

P.never_panicsmd entry input

Proof 19 steps Qed

intros Hm Hf Hd Ha Hn Hwp

apply L.wp_never_panicsHasNoLc Σ md entry input globals m f Hm Hf

intros xs Hxs

destruct Hwpxs Hxs as fr & Hfr & Hw

exists fr

split ; exact Hfr |

intros Hready fuel Hinv

iMod gen_heap_initlist_to_mapps : gmappiece pval as HheapG (Hh & Hpts & _)

iModIntro

iExists heap_interpno_world

iSplitL Hh

–iExists _

iFrame Hh

iPureIntro

split ; | split ; exact Hd | split ; exact Hready | exact I

intros l v Hl

exact all_agree_elem_ _ _ _ Ha elem_of_list_to_map_2_ _ _ Hl

–iApply HwHinv HheapG

rewrite / pts - big_sepM_list_to_mapλl v ⇒ pointstol DfracOwn1 v ; iExact Hpts | exact Hn

The resources the proofs use: invariants and the ghost heap.

145Definition glibcΣ: gFunctors ≔

#invΣ; gen_heapΣpiece pval

glibcΣ has invariants.

148Instance glibcΣ_inv: invGpreSglibcΣ

Proof 2 steps Qed

apply subG_invΣ

apply _

glibcΣ has the ghost heap of pieces.

152Instance glibcΣ_heap: gen_heapGpreSpiece pval glibcΣ

Proof 2 steps Qed

apply subG_gen_heapGpreS

apply _