26 - Derived rules and proof automation for C light

Summary

For convenient application of the VST program logic for C light, we have synthetic or derived rules: lemmas built from common combinations of the primitive inference rules for C light. We also have proof automation: programs that look at proof goals and choose which rules to apply.

For example, consider the C-language statements x:=e→f; and e1→f := e2; where x is a variable, f is the name of a structure field, and e, e1, e2 are expressions. The first command is a load field statement, and the second is a store field. Proofs about these statements could be done using the general semax-load and semax-store rules—along with the mapsto operator—but these require a lot of reasoning about field l-values. It's best to define a synthetic field_mapsto predicate that can be used as if it were a primitive:

Definition field-mapsto (sh:share)(t1:type)(fld:ident)(v1 v2: val): mpred.

We do not show the definition here (see floyd/field_mapsto.v) but basically field_mapsto π τ v₁v₂ is a predicate meaning: τ is a struct type whose field f of type τ₂ has address-offset δ from the base address of the struct; the size/signedness of f is ch, v₁ is a pointer to a struct of type τ, and the heaplet contains exactly v₁ + δ v₂, (value v₂ at address v₁ + δ with permission-share π), where v₂: τ₂.