Logics for Resource Consumption

This page summarises the logics for resource consumption we developed in the MRG project. The first section decribes the rules of the Grail bytecode logic (or core logic), which is a VDM-style program logic for a subset of the JVM language. The second section then discusses the heap space logic (or MRG logic) built on top of this core logic for reasoning about heap consumption. Details of these logics can be found in the following two papers:

This document is intended as a reference page for the rules of the Grail logic when hacking your own certificates, or extending the MRG proving infrastructure. It complements the User's Guide for the MRG infrastructure. If you want to learn more about the design of the logics and their properties, lookup the above papers.

Grail Bytecode Logic

Below are the rules for the program logic for Grail (or "Bytecode Logic"). We use a shallow embedding to formalise assertions, which have the type env × heap × heap × val × rescomp ⇒ bool A judgement in the Bytecode Logic has the form G ⊳ e : P, where e is a Grail expression, P is an assertion and G is a context mapping expressions to assertions. The following constants are used
tickRo ≡ ⟨1 0 0 0⟩

Logic Rules

vdm_null: G ⊳ (NULL hint): (λ E h hh v p . hh = h ∧ v = RVal Nullref ∧ p = tickRo
vdm_int: G ⊳ Int i : (λ E h hh v p . hh = h ∧ v = IVal i ∧ p = tickRo
vdm_ivar: G ⊳ IVar x : λ E h hh v p . hh = h ∧ v = IVal (E⟨x⟩) ∧ p = tickRo
vdm_rvar: G ⊳ RVar x : λ E h hh v p . hh = h ∧ v = RVal (E⌊x⌋) ∧ p = tickRo
vdm_prim: G ⊳ Primop f x y : λ E h hh v p . hh = h ∧ v = IVal (f (E⟨x⟩) (E⟨y⟩)) ∧ p = ⟨3 0 0 0⟩
vdm_rprim: G ⊳ RPrimop f x y : λ E h hh v p . hh = h ∧ v = IVal (f (E⌊x⌋) (E⌊y⌋)) ∧ p = ⟨3 0 0 0⟩
vdm_getfi: G ⊳ GetFi x f : λ E h hh v p . ∃ a . E⌊x⌋ = Ref a ∧ a∈Dom h ∧ hh = h ∧ v = IVal (h) ∧ p = ⟨2 0 0 0⟩
vdm_getfr: G ⊳ GetFr x f : λ E h hh v p . ∃ a . E⌊x⌋ = Ref a ∧ a∈Dom h ∧ hh = h ∧ v = RVal (h⌊a♦f⌋) ∧ p = ⟨2 0 0 0⟩
vdm_putfi: G ⊳ PutFi x f y : (λ E h hh v p . ∃ a . E⌊x⌋ = Ref a ∧ a∈Dom h ∧ hh = h ∧ v = arbitrary ∧ p = ⟨3 0 0 0⟩
vdm_putfr: G ⊳ PutFr x f y : (λ E h hh v p . ∃ a . E⌊x⌋ = Ref a ∧ a∈Dom h ∧ hh = h⌊a♦f:=E⌊y⌋⌋ ∧ v = arbitrary ∧ p = ⟨3 0 0 0⟩
vdm_getstat: G ⊳ GetStat c f : (λ E h hh v p . h = hh ∧ v = RVal (h { c♦f }) ∧ p = ⟨2 0 0 0⟩
vdm_new: G ⊳ New c ifldvals rfldvals : (λ E h hh v p . ∃ l . l = freshloc (fmap_dom (heap.oheap h)) ∧ hh = newObj h l E c ifldvals rfldvals ∧ v = RVal (Ref l) ∧ p = tickRo
vdm_if:
〚G ⊳ e1 : P1; G ⊳ e2 : P2〛
G ⊳ (IF x THEN e1 ELSE e2) : (λ E h hh v p . ∃ pp. p = tkn 2 pp ∧ (E⟨x⟩ = grailbool True → (P1 E h hh v pp )) ∧ (E⟨x⟩ = grailbool False → (P2 E h hh v pp )) ∧ (E⟨x⟩ = grailbool True ∨ E⟨x⟩ = grailbool False)
vdm_leti:
〚G ⊳ e1 : P1; G ⊳ e2 : P2〛
G ⊳ (Leti x e1 e2) : (λ E h hh v p . ∃ p1 p2 h1 i . (P1 E h h1 (IVal i) p1) ∧ (P2 (E⟨x&assign;i⟩) h1 hh v p2) ∧ p = tk (p1 ⌣ p2)
vdm_letr:
〚G ⊳ e1 : P1; G ⊳ e2 : P2〛
G ⊳ (Letr x e1 e2) : (λ E h hh v p . ∃ p1 p2 h1 r . (P1 E h h1 (RVal r) p1) ∧ (P2 (E⌊x:=r⌋) h1 hh v p2) ∧ p = tk (p1 ⌣ p2)
vdm_letv:
〚G ⊳ e1 : P1; G ⊳ e2 : P2〛
G ⊳ (Letv e1 e2) : (λ E h hh v p . ∃ p1 p2 h1 w . (P1 E h h1 w p1) ∧ (P2 E h1 hh v p2) ∧ p = (p1 ⌣ p2)
vdm_call:
〚 ({(Call f, P)} ⋃ G) ⊳ snd(funtable f) : (λ E h hh v p . (P E h hh v (tkcall p)))〛
G ⊳ (Call f) : P
vdm_invokestatic:
〚({(C•mn(args),P)} ⋃ G) ⊳ (snd (methtable C mn)) : (λ E h hh v p . ∀ E'. (Nullref, fst (methtable C mn), args,E',E) : FRAME → (P E' h hh v (⟨3 0 1 1⟩ ⊕ p) )) 〛
G ⊳ (C•mn(args)) : P
vdm_invoke:
〚 ∀ C . ({(x♦mn(args),P)} ⋃ G) ⊳ (snd (methtable C mn)) : (λ E h hh v p . ∀ E' . classOf E' h x C ∧ (E'⌊x⌋, fst (methtable C mn), args,E',E) : FRAME → (P E' h hh v (⟨5 0 1 1⟩ ⊕ p) )) 〛
G ⊳ (x♦mn(args)) : P
vdm_ax:
〚 (e,P) : G 〛
G ⊳ e : P
vdm_conseq:
〚G ⊳ e : P; (∀ E h hh v p . (P E h hh v p ) → (Q E h hh v p ))〛
G ⊳ e : Q

Logic Properties

The main soundness theorem of the logic is as follows:
theorem vdm_sound_ctxt: G ⊳ e:P ⇒ G ⊨ e:P

Here is a summary of the main definitions related to validity of assertions:

constdefs vdm_validn :: nat ⇒ expr ⇒ vdmassn ⇒ bool" ("⊨_ _ : _" 50)
"⊨n e : P ≡ (∀ m . m ≤ n → (∀ E h hh v p . ((E ⊢ h,e ⇓m (hh,v,p)) → P E h hh v p)))"

constdefs vdm_valid :: " expr ⇒ vdmassn ⇒ bool" ("⊨ _ : _" 50)
"⊨ e : P ≡ (∀ E h hh v p . ((E ⊢ h,e ⇓ hh,v,p) → P E h hh v p))"

constdefs vdm_context_validn::"nat ⇒ vdmcontext ⇒ bool" ("⊢_ _" 60)
"⊢n G ≡ (∀ (e,P) ∈ G . ⊨n e : P)"

constdefs vdm_context_valid::" vdmcontext ⇒ bool" ("⊢ _" 60)
"⊢ G ≡ (∀ (e,P) ∈ G . ⊨ e : P)"

Heap Space Logic

The rules of this logic have the form MRG_c where c is a constructor in the syntax of Grail (e.g. MRG_Leti): MRG_Int, MRG_IVar, MRG_RVar, MRG_Prim, MRG_RPrim, MRG_NullList, MRG_NullRes, MRG_NullTree, MRG_NullList, MRG_NullRes, MRG_NullTree, MRG_Letv, MRG_Leti, MRG_Letr, MRG_LetrNull, MRG_If, MRG_ListMatch, MRG_ListMatchD, MRG_MakeList, MRG_MakeList_ml, MRG_ResultMatch, MRG_ResultMatchD, MRG_MakeResultSome, MRG_TreeMatch, MRG_TreeMatchD, MRG_MakeTree, MRG_InvStat, MRG_Call, MRG_Weak, lemma MRG. The main soundness theorem of the heap space logic is

theorem MRG_sound: (G,e,U,n,C,T,m) ∈ MRG ⇒ G ⊳ e : 〚 U, n, C » T, m 〛

Useful tactics that combine these rules are LEAF, for all leaf cases of the logic, CALL for function calls, RENA for applying renamings etc. Useful tactics for simplification are GT for getting an element from a context. Lemmas with definitions of program code are collected in meth_defs and f_pdefs for each function f. The lemmas dmp_defs contain definitions for the dominates and the merge point sets, and ctxt_defs for the definition of the context.

The DOM_Call relation is a logic for proving derived assertions for functions, using the dominates information proved by the compiler. It's defined inductively over its first argument, a list, with rules DOM_CallNil and DOM_CallCONS. The tactics DOM (and DOMS for a 1-step version) use these rules.