# PCC Instantiation - Overflow & Type safety for SAL

 In these theories we instantiate our Proof Carrying Code Framework to a simple assembly language (SAL) with a safety policy that prohibits arithmetic overflows and type errors. As safety logic we use a variant of first order arithmetics in form of a deep embedding. Safety Proofs can be conducted in Isabelle using the Isabelle/HOL inference rules. From the framework we get a verified, executable VCG, which we use to certify the safety of various SAL programs. The safety proofs can be checked using Isabelle/HOL's proof checker.

 Machine Code: SAL Safety Policy: No overflows, No type errors Safety Logic: FOA (deep embedding)
 SALSyntax.thy [pdf] Simple Assembly Language (SAL) instructions and datatypes. FiniteMap.thy [pdf] Finite Maps are use for substitution functions. DeepLogic.thy [pdf] Syntax (dataype form) and manipulation of formulae (substitution functions). SALSemantics_deep.thy [pdf] The meaning of SAL programs in form of a small step semantics. SALSafetyLogic_deep.thy [pdf] Instantiates the safety logic (connectives, judgements), the safety policy (safeF), and VCG parameter functions (succsF, wpF). SALOverflowPlatform.thy [pdf] Instantiates the VCG and a wellformedness checker for SAL programs. SALOverflowFWInst.thy [pdf] Shows that all instantiations satisfy the requirements of the PCC Framework. Establishes the VCG Soundness theorem for this platform. VCOpt.thy [pdf] Defines and verifies an optimizer for verification conditions.

## Examples

 EX_DoubleAddition_deep.thy [pdf] Very primitive example: Computes 4 times X using two additions. EX_SmartCardPurse.thy [pdf] A check procedure protects the balance of a smart card purse from overflows. EX_RecMult_deep.thy [pdf] Multiplies two numbers with a recursive procedure; uses pointers to simulate a call stack in memory.