Theory Cachera
theory Cachera imports Logic begin
section‹A derived logic for a strong type system›
text‹In this section we consider a system of derived assertions, for
a type system for bounded heap consumption. The type system arises by
reformulating the analysis of Cachera, Jensen, Pichardie, and
Schneider \<^cite>‹"CaJePiSc05MemoryUsage"› for a high-level functional
language. The original approach of Cachera et al.~consists of
formalising the correctness proof of a certain analysis technique in
Coq. Consequently, the verification of a program requires the
execution of the analysis algorithm inside the theorem prover, which
involves the computation of the (method) call graph and fixed point
iterations. In contrast, our approach follows the proof-carrying code
paradigm more closely: the analysis amounts to a type inference which
is left unformalised and can thus be carried out outside the trusted
code base. Only the result of the analysis is communicated to the code
recipient. The recipient verifies the validity of the certificate by
a largely syntax-directed single-pass traversal of the (low-level)
code using a domain-specific program logic. This approach to
proof-carrying code was already explored in the MRG project, with
respect to program logics of partial correctness
\<^cite>‹"BeringerHofmannMomiglianoShkaravska:LPAR2004"› and a type system
for memory consumption by Hofmann and
Jost~\<^cite>‹"HofmannJost:POPL2003"›. In order to obtain
syntax-directedness of the proof rules, these had to be formulated at
the granularity of typing judgements. In contrast, the present proof
system admits proof rules for individual JVM instructions.
Having derived proof rules for individual JVM instructions, we
introduce a type system for a small functional language, and a
compilation into bytecode. The type system associates a natural
number $n$ to an expression $e$, in a typing context
$\Sigma$. Informally, the interpretation of a typing judgement
$\Sigma \rhd e:n$ is that the evaluation of $e$ (which may include
the invocation of functions whose resource behaviour is specified in
$\Sigma$) does not perform more than $n$ allocations. The type system
is then formally proven sound, using the derived logic for bytecode.
By virtue of the invariants, the guarantee given by the present system
is stronger than the one given by our encoding of the Hofmann-Jost
system, as even non-terminating programs can be verified in a
meaningful way.›
subsection‹Syntax and semantics of judgements›
text‹The formal interpretation at JVM level of a type ‹n› is
given by a triple $$\mathit{Cachera}(n) = (A, B, I)$$ consisting of a
(trivial) precondition, a post-condition, and a strong invariant.›
definition Cachera::"nat ⇒ (Assn × Post × Inv)" where
"Cachera n = (λ s0 s . True,
λ s0 (ops,s,h) (k,v) . |k| ≤ |h| + n,
λ s0 (ops,s,h) k. |k| ≤ |h| + n)"
text‹This definition is motivated by the expectation that $\rhd
\lbrace A \rbrace\; \ulcorner\, e \urcorner\, \lbrace B \rbrace\, I$
should be derivable whenever the type judgement $\Sigma \rhd e:n$
holds, where $ \ulcorner e \urcorner$ is the translation of compiling
the expression $e$ into JVML, and the specification table ‹MST›
contains the interpretations of the entries in $\Sigma$.›
text‹We abbreviate the above construction of judgements by a
predicate ‹deriv›.›
definition deriv::"CTXT ⇒ Class ⇒ Method ⇒ Label ⇒
(Assn × Post × Inv) ⇒ bool" where
"deriv G C m l (ABI) = (let (A,B,I) = ABI in (G ⊳ ⦃ A ⦄ C,m,l ⦃ B ⦄ I))"
text‹Thus, the intended interpretation of a typing judgement $\Sigma
\rhd e: n$ is $$\mathit{deriv}\; C\; m\; l\; (\mathit{Cachera}\; n)$$
if $e$ translates to a code block whose first instruction is at
$C.m.l$.›
text‹We also define a judgement of the auxiliary form of
sequents.›
definition derivAssum::"CTXT ⇒ Class ⇒ Method ⇒ Label ⇒
(Assn × Post × Inv) ⇒ bool" where
"derivAssum G C m l (ABI) = (let (A,B,I) = ABI in G ⊳ ⟨ A ⟩ C,m,l ⟨ B ⟩ I)"
text‹The following operation converts a derived judgement into the
syntactical form of method specifications.›
definition mkSPEC::"(Assn × Post × Inv) ⇒ ANNO ⇒
(MethSpec × MethInv × ANNO)" where
"mkSPEC (ABI) Anno = (let (A,B,I) = ABI in
(λ s0 t . B s0 (mkState s0) t, λ s0 h . I s0 (mkState s0) h, Anno))"
text‹This enables the interpretation of typing contexts $\Sigma$ as a
set of constraints on the specification table ‹MST›.›
subsection‹Derived proof rules›
declare Let_def[simp]
text‹We are now ready to prove derived rules, i.e.~proof rules where
assumptions as well as conclusions are of the restricted assertion
form. While their justification unfolds the definition of the
predicate ‹deriv›, their application will not. We first give
syntax-directed proof rules for all JVM instructions:›
lemma CACH_NEW:
"⟦ ins_is C m l (new c); MST↓(C,m)=Some(Mspec,Minv,Anno);
Anno↓(l) = None; n = k + 1; derivAssum G C m (l+1) (Cachera k) ⟧
⟹ deriv G C m l (Cachera n)"
apply (simp add: ins_is_def Cachera_def deriv_def derivAssum_def, clarsimp)
apply (rule INSTR) apply assumption+ apply simp apply (simp add: heap_def)
apply fast
apply (erule CONSEQ)
apply (simp add: SP_pre_def)
apply clarsimp apply (simp add: SP_post_def) apply clarsimp
apply (drule NewElim1, fastforce) apply clarsimp
apply (subgoal_tac "ba↓(nextLoc ba) = None")
apply (simp add: AL_Size_UpdateSuc)
apply (rule nextLoc_fresh)
apply clarsimp
apply (simp add: SP_inv_def)
apply clarsimp
apply (drule NewElim1, fastforce) apply clarsimp
apply (subgoal_tac "ba↓(nextLoc ba) = None")
apply (simp add: AL_Size_UpdateSuc)
apply (rule nextLoc_fresh)
done
lemma CACH_INSTR:
"⟦ ins_is C m l I;
I ∈ { const c, dup, pop, swap, load x, store x, binop f,
unop g, getfield d F, putfield d F, checkcast d};
MST↓(C,m)=Some(Mspec,Minv,Anno); Anno↓(l) = None;
derivAssum G C m (l+1) (Cachera n) ⟧
⟹ deriv G C m l (Cachera n)"
apply (simp add: ins_is_def Cachera_def deriv_def derivAssum_def, clarsimp)
apply (rule INSTR) apply assumption+ apply simp apply (simp add: heap_def)
apply fast
apply (erule CONSEQ)
apply (simp add: SP_pre_def)
apply (simp add: SP_post_def) apply clarsimp
apply safe
apply (drule ConstElim1, fastforce) apply clarsimp
apply (drule DupElim1, fastforce) apply clarsimp
apply (drule PopElim1, fastforce) apply clarsimp
apply (drule SwapElim1, fastforce) apply clarsimp
apply (drule LoadElim1, fastforce) apply clarsimp
apply (drule StoreElim1, fastforce) apply clarsimp
apply (drule BinopElim1, fastforce) apply clarsimp
apply (drule UnopElim1, fastforce) apply clarsimp
apply (drule GetElim1, fastforce) apply clarsimp
apply (drule PutElim1, fastforce) apply clarsimp
apply (simp add: updSize)
apply (drule CastElim1, fastforce) apply clarsimp
apply (simp_all add: SP_inv_def)
apply safe
apply (drule ConstElim1, fastforce) apply clarsimp
apply (drule DupElim1, fastforce) apply clarsimp
apply (drule PopElim1, fastforce) apply clarsimp
apply (drule SwapElim1, fastforce) apply clarsimp
apply (drule LoadElim1, fastforce) apply clarsimp
apply (drule StoreElim1, fastforce) apply clarsimp
apply (drule BinopElim1, fastforce) apply clarsimp
apply (drule UnopElim1, fastforce) apply clarsimp
apply (drule GetElim1, fastforce) apply clarsimp
apply (drule PutElim1, fastforce) apply clarsimp
apply (simp add: updSize)
apply (drule CastElim1, fastforce) apply clarsimp
done
lemma CACH_RET:
"⟦ ins_is C m l vreturn; MST↓(C,m)=Some(Mspec,Minv,Anno);
Anno↓(l) = None ⟧
⟹ deriv G C m l (Cachera 0)"
apply (simp add: ins_is_def Cachera_def deriv_def derivAssum_def, clarsimp)
apply (rule VRET) apply assumption+ apply simp apply (simp add: heap_def)
apply clarsimp
done
lemma CACH_GOTO:
"⟦ ins_is C m l (goto pc); MST↓(C,m)=Some(Mspec,Minv,Anno);
Anno↓(l) = None; derivAssum G C m pc (Cachera n) ⟧
⟹ deriv G C m l (Cachera n)"
apply (simp add: ins_is_def Cachera_def deriv_def derivAssum_def, clarsimp)
apply (rule GOTO) apply assumption+ apply simp apply (simp add: heap_def)
apply (erule CONSEQ)
apply (simp add: SP_pre_def)
apply (simp add: SP_post_def) apply clarsimp apply (drule GotoElim1, fastforce)
apply clarsimp
apply (simp add: SP_inv_def) apply clarsimp apply (drule GotoElim1, fastforce)
apply clarsimp
done
lemma CACH_IF:
"⟦ ins_is C m l (iftrue pc); MST↓(C,m)=Some(Mspec,Minv,Anno);
Anno↓(l) = None; derivAssum G C m pc (Cachera n);
derivAssum G C m (l+1) (Cachera n) ⟧
⟹ deriv G C m l (Cachera n)"
apply (simp add: ins_is_def Cachera_def deriv_def derivAssum_def, clarsimp)
apply (rule IF) apply assumption+ apply (simp, simp add: heap_def)
apply (erule CONSEQ)
apply (simp add: SP_pre_def)
apply (simp add: SP_post_def) apply clarsimp apply (drule IfElim1, fastforce) apply clarsimp
apply (simp add: SP_inv_def) apply clarsimp apply (drule IfElim1, fastforce) apply clarsimp
apply clarsimp
apply (erule CONSEQ)
apply (simp add: SP_pre_def)
apply (simp add: SP_post_def) apply clarsimp apply (drule IfElim1, fastforce) apply clarsimp
apply (simp add: SP_inv_def) apply clarsimp apply (drule IfElim1, fastforce) apply clarsimp
done
lemma CACH_INVS:
"⟦ ins_is C m l (invokeS D m'); mbody_is D m' (par,code,l0);
MST↓(C,m)=Some(Mspec,Minv,Anno); Anno↓(l) = None;
MST↓(D, m') = Some(mkSPEC (Cachera k) Anno2);
nk = n+k; derivAssum G C m (l+1) (Cachera n)⟧
⟹ deriv G C m l (Cachera nk)"
apply (simp add: ins_is_def Cachera_def deriv_def derivAssum_def, clarsimp)
apply (rule INVS) apply assumption+
apply (simp add: mkSPEC_def) apply fastforce apply simp apply (simp add: heap_def)
apply (simp add: mkState_def)
apply (erule CONSEQ)
apply clarsimp
apply clarsimp apply (simp add: SINV_post_def mkState_def)
apply clarsimp apply (simp add: SINV_inv_def mkState_def)
done
text‹In addition, we have two rules for subtyping›
lemma CACH_SUB:
"⟦ deriv G C m l (Cachera n); n ≤ k⟧ ⟹ deriv G C m l (Cachera k)"
apply (simp add: deriv_def derivAssum_def Cachera_def)
apply (rule CONSEQ, assumption+)
apply simp
apply simp
apply simp
done
lemma CACHAssum_SUB:
"⟦ derivAssum G C m l (Cachera n); n ≤ k⟧
⟹ derivAssum G C m l (Cachera k)"
apply (simp add: derivAssum_def Cachera_def)
apply (rule CONSEQ, assumption+)
apply simp
apply simp
apply simp
done
text‹and specialised forms of the axiom rule and the injection rule.›
lemma CACH_AX:
"⟦ G↓(C,m,l) = Some (Cachera n); MST↓(C,m)=Some(Mspec,Minv,Anno);
Anno↓(l) = None⟧
⟹ derivAssum G C m l (Cachera n)"
apply (simp add: derivAssum_def Cachera_def)
apply (drule AX) apply assumption apply simp apply (simp add: heap_def)
apply (rule CONSEQ) apply assumption+ apply simp apply simp apply simp
done
lemma CACH_INJECT:
"deriv G C m l (Cachera n) ⟹ derivAssum G C m l (Cachera n)"
apply (simp add: deriv_def derivAssum_def Cachera_def)
apply (erule INJECT)
done
text‹Finally, a verified-program rule relates specifications to
judgements for the method bodies. Thus, even the method specifications
may be given as derived assertions (modulo the ‹mkSPEC›-conversion).›
lemma CACH_VP:
"⟦ ∀ c m par code l0. mbody_is c m (par, code, l0) ⟶
(∃ n Anno . MST↓(c,m) = Some(mkSPEC(Cachera n) Anno) ∧
deriv G c m l0 (Cachera n));
∀ c m l A B I. G↓(c,m,l) = Some(A,B,I) ⟶
(∃ n . (A,B,I) = Cachera n ∧ deriv G c m l (Cachera n))⟧
⟹ VP"
apply (simp add: VP_def) apply (rule_tac x=G in exI, simp add: VP_G_def)
apply safe
apply (erule thin_rl)
apply (erule_tac x=C in allE, erule_tac x=m in allE, erule_tac x=l in allE, clarsimp)
apply (simp add: deriv_def)
apply (rotate_tac 1, erule thin_rl)
apply (erule_tac x=C in allE, erule_tac x=m in allE)
apply(erule_tac x=par in allE, erule_tac x=code in allE, erule_tac x=l0 in allE, clarsimp)
apply (simp add: Cachera_def mkSPEC_def deriv_def, clarsimp)
apply (rule CONSEQ) apply assumption+
apply simp
apply (simp add: mkPost_def mkState_def)
apply (simp add: mkState_def mkInv_def)
done
subsection‹Soundness of high-level type system›
text‹We define a first-order functional language where expressions
are stratified into primitive expressions and general expressions. The
language supports the construction of lists using constructors
$\mathit{NilPrim}$ and $\mathit{ConsPrim}\; h\; t$, and includes a
corresponding pattern match operation. In order to simplify the
compilation, function identifiers are taken to be pairs of class names
and method names.›
type_synonym Fun = "Class × Method"