Ghost Code

What is ghost code?

ghost code is part of the program that is added for the purpose of specification

Why3 team, “The Spirit of Ghost Code”

... or verification

addition by SPARK team

  • Examples of ghost code:

    • contracts (Pre, Post, Contract_Cases, etc.)
    • assertions (pragma Assert, loop (in)variants, etc.)
    • special values Func'Result, Var'Old, Var'Loop_Entry
  • Is it enough?

Ghost code – A trivial example

  • how to express it?
package Show_Trivial_Example is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array; Free : Natural; procedure Alloc; end Show_Trivial_Example;
package body Show_Trivial_Example is procedure Alloc is begin -- some computations here -- -- assert that Free “increases” null; end Alloc; end Show_Trivial_Example;

Ghost variables – aka auxiliary variables

  • Variables declared with aspect Ghost

    • declaration is discarded by compiler when ghost code ignored
  • Ghost assignments to ghost variables

    • assignment is discarded by compiler when ghost code ignored
package Show_Ghost_Variable is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array; Free : Natural; procedure Alloc; end Show_Ghost_Variable;
package body Show_Ghost_Variable is procedure Alloc is Free_Init : Natural with Ghost; begin Free_Init := Free; -- some computations here pragma Assert (Free > Free_Init); end Alloc; end Show_Ghost_Variable;

Ghost variables – non-interference rules

  • Ghost variable cannot be assigned to non-ghost one

    • Free := Free_Init;
  • Ghost variable cannot indirectly influence assignment to non-ghost one

if Free_Init < Max then
   Free := Free + 1;
end if;
procedure Show_Non_Interference is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array; Free : Natural; Free_Init : Natural with Ghost; procedure Alloc is begin Free_Init := Free; -- some computations here pragma Assert (Free > Free_Init); end Alloc; procedure Assign (From : Natural; To : out Natural) is begin To := From; end Assign; begin Assign (From => Free_Init, To => Free); end Show_Non_Interference;

Ghost statements

  • Ghost variables can only appear in ghost statements

    • assignments to ghost variables
    • assertions and contracts
    • calls to ghost procedures
procedure Show_Ghost_Statements is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array; Free : Natural; Free_Init : Natural with Ghost; procedure Alloc is begin Free_Init := Free; -- some computations here pragma Assert (Free > Free_Init); end Alloc; procedure Assign (From : Natural; To : out Natural) with Ghost is begin To := From; end Assign; begin Assign (From => Free, To => Free_Init); end Show_Ghost_Statements;
procedure Show_Ghost_Statements is
begin
   --  Non-ghost variable "Free" cannot appear as actual in
   --  call to ghost procedure
   Assign (From => Free_Init, To => Free);
end Show_Ghost_Statements;

Ghost procedures

  • Ghost procedures cannot write into non-ghost variables
procedure Assign (Value : Natural) with Ghost is
begin
   --  "Free" is a non-ghost variable
   Free := Value;
end Assign;
  • Used to group statements on ghost variables

    • in particular statements not allowed in non-ghost procedures
procedure Assign_Cond (Value : Natural) with Ghost is
begin
   if Condition then
      Free_Init := Value;
   end if;
end Assign_Cond;
  • Can have Global (including Proof_In) & Depends contracts

Ghost functions

  • Functions for queries used only in contracts

  • Typically implemented as expression functions

    • in private part – proof of client code can use expression
    • or in body – only proof of unit can use expression
package Show_Ghost_Function is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array; Free : Natural; Free_Init : Natural with Ghost; procedure Alloc with Pre => Free_Memory > 0, Post => Free_Memory < Free_Memory'Old; function Free_Memory return Natural with Ghost; private -- Completion of ghost function declaration function Free_Memory return Natural is (0); -- dummy implementation -- If function body as declaration: -- -- function Free_Memory return Natural is (...) with Ghost; end Show_Ghost_Function;

Imported ghost functions

  • Ghost functions without a body

    • cannot be executed
function Free_Memory return Natural with Ghost, Import;
  • Typically used with abstract ghost private types

    • definition in SPARK_Mode(Off)

      • type is abstract for GNATprove
package Show_Imported_Ghost_Function with SPARK_Mode => On is type Memory_Chunks is private; function Free_Memory return Natural with Ghost; function Free_Memory return Memory_Chunks with Ghost, Import; private pragma SPARK_Mode (Off); type Memory_Chunks is null record; end Show_Imported_Ghost_Function;
  • Definition of ghost types/functions given in proof

    • either in Why3 using External_Axiomatization
    • or in an interactive prover (Coq, Isabelle, etc.)

Ghost packages and ghost abstract state

  • Every entity in a ghost package is ghost

    • local ghost package can group all ghost entities
    • library-level ghost package can be withed/used in regular units
  • Ghost abstract state can only represent ghost variables

package Show_Ghost_Package with Abstract_State => (State with Ghost) is function Free_Memory return Natural with Ghost; end Show_Ghost_Package;
package body Show_Ghost_Package with Refined_State => (State => (Data, Free, Free_Init)) is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array with Ghost; Free : Natural with Ghost; Free_Init : Natural with Ghost; function Free_Memory return Natural is (0); -- dummy implementation end Show_Ghost_Package;
  • Non-ghost abstract state can contain both ghost and non-ghost variables

Executing ghost code

  • Ghost code can be enabled globally

    • using compilation switch -gnata (for all assertions)
  • Ghost code can be enabled selectively

    • using pragma Assertion_Policy (Ghost => Check)
    • SPARK rules enforce consistency – in particular no write disabled
package Show_Exec_Ghost_Code is pragma Assertion_Policy (Ghost => Check); -- pragma Assertion_Policy (Ghost => Ignore, Pre => Check); procedure Alloc with Pre => Free_Memory > 0; function Free_Memory return Natural with Ghost; end Show_Exec_Ghost_Code;
  • GNATprove analyzes all ghost code and assertions

Examples of use

Encoding a state automaton

  • Tetris in SPARK

  • Global state encoded in global ghost variable

    • updated at the end of procedures of the API
type State is (Piece_Falling, ...) with Ghost;
Cur_State : State with Ghost;
  • Properties encoded in ghost functions
function Valid_Configuration return Boolean is
   (case Cur_State is
      when Piece_Falling => ...,
      when ...)
with Ghost;

Expressing useful lemmas

  • GCD in SPARK

  • Lemmas expressed as ghost procedures

procedure Lemma_Not_Divisor (Arg1, Arg2 : Positive) with
   Ghost,
   Global => null,
   Pre  => Arg1 in Arg2 / 2 + 1 .. Arg2 - 1,
   Post => not Divides (Arg1, Arg2);
  • Most complex lemmas further refined into other lemmas

    • code in procedure body used to guide proof (e.g. for induction)

Specifying an API through a model

  • Red black trees in SPARK

  • Invariants of data structures expressed as ghost functions

    • using Type_Invariant on private types
  • Model of data structures expressed as ghost functions

    • called from Pre / Post of subprograms from the API
  • Lemmas expressed as ghost procedures

    • sometimes without contracts to benefit from inlining in proof

Extreme proving with ghost code – red black trees in SPARK

../../../_images/ghost_code_red_black.png

Positioning ghost code in proof techniques

../../../_images/ghost_code_degree_of_automation.png

Code Examples / Pitfalls

Example #1

procedure Example_01 is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array; Free : Natural; procedure Alloc is Free_Init : Natural with Ghost; begin Free_Init := Free; -- some computations here if Free <= Free_Init then raise Program_Error; end if; end Alloc; begin null; end Example_01;

This code is not correct. A ghost entity cannot appear in this context.

Example #2

procedure Example_02 is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array; Free : Natural; procedure Alloc is Free_Init : Natural with Ghost; procedure Check with Ghost is begin if Free <= Free_Init then raise Program_Error; end if; end Check; begin Free_Init := Free; -- some computations here Check; end Alloc; begin null; end Example_02;

This code is correct. Note that procedure Check is inlined for proof (no contract).

Example #3

package Example_03 is type Data_Array is array (1 .. 10) of Integer; Data : Data_Array; Free : Natural; pragma Assertion_Policy (Pre => Check); procedure Alloc with Pre => Free_Memory > 0; function Free_Memory return Natural with Ghost; end Example_03;

This code is not correct. Incompatible ghost policies in effect during compilation, as ghost code is ignored by default. Note that GNATprove accepts this code as it enables all ghost code and assertions.

Example #4

package Example_04 is procedure Alloc with Post => Free_Memory < Free_Memory'Old; function Free_Memory return Natural with Ghost; end Example_04;
package body Example_04 is Free : Natural; Max : constant := 1000; function Free_Memory return Natural is begin return Max - Free + 1; end Free_Memory; procedure Alloc is begin Free := Free + 10; end Alloc; end Example_04;

This code is not correct. No postcondition on Free_Memory that would allow proving the postcondition on Alloc.

Example #5

package Example_05 is procedure Alloc with Post => Free_Memory < Free_Memory'Old; function Free_Memory return Natural with Ghost; end Example_05;
package body Example_05 is Free : Natural; Max : constant := 1000; function Free_Memory return Natural is (Max - Free + 1); procedure Alloc is begin Free := Free + 10; end Alloc; end Example_05;

This code is correct. Free_Memory has an implicit postcondition as an expression function.

Example #6

procedure Example_06 is subtype Resource is Natural range 0 .. 1000; subtype Num is Natural range 0 .. 6; subtype Index is Num range 1 .. 6; type Data is array (Index) of Resource; function Sum (D : Data; To : Num) return Natural is (if To = 0 then 0 else D (To) + Sum (D, To - 1)) with Ghost; procedure Create (D : out Data) with Post => Sum (D, D'Last) < 42 is begin for J in D'Range loop D (J) := J; pragma Loop_Invariant (2 * Sum (D, J) <= J * (J + 1)); end loop; end Create; begin null; end Example_06;

This code is not correct. Info: expression function body not available for proof (Sum may not return).

Example #7

procedure Example_07 is subtype Resource is Natural range 0 .. 1000; subtype Num is Natural range 0 .. 6; subtype Index is Num range 1 .. 6; type Data is array (Index) of Resource; function Sum (D : Data; To : Num) return Natural is (if To = 0 then 0 else D (To) + Sum (D, To - 1)) with Ghost, Annotate => (GNATprove, Terminating); procedure Create (D : out Data) with Post => Sum (D, D'Last) < 42 is begin for J in D'Range loop D (J) := J; pragma Loop_Invariant (2 * Sum (D, J) <= J * (J + 1)); end loop; end Create; begin null; end Example_07;

This code is correct. Note that GNATprove does not prove the termination of Sum here.

Example #8

procedure Example_08 is subtype Resource is Natural range 0 .. 1000; subtype Num is Natural range 0 .. 6; subtype Index is Num range 1 .. 6; type Data is array (Index) of Resource; function Sum (D : Data; To : Num) return Natural is (if To = 0 then 0 else D (To) + Sum (D, To - 1)) with Ghost, Annotate => (GNATprove, Terminating); procedure Create (D : out Data) with Post => Sum (D, D'Last) < 42 is begin for J in D'Range loop D (J) := J; end loop; end Create; begin null; end Example_08;

This code is correct. The loop is unrolled by GNATprove here, as D'Range is 0 .. 6. The automatic prover unrolls the recursive definition of Sum.

Example #9

with Ada.Containers.Functional_Vectors; procedure Example_09 is subtype Resource is Natural range 0 .. 1000; subtype Index is Natural range 1 .. 42; package Seqs is new Ada.Containers.Functional_Vectors (Index, Resource); use Seqs; function Create return Sequence with Post => (for all K in 1 .. Last (Create'Result) => Get (Create'Result, K) = K) is S : Sequence; begin for K in 1 .. 42 loop S := Add (S, K); end loop; return S; end Create; begin null; end Example_09;

This code is not correct. Loop requires a loop invariant to prove the postcondition.

Example #10

with Ada.Containers.Functional_Vectors; procedure Example_10 is subtype Resource is Natural range 0 .. 1000; subtype Index is Natural range 1 .. 42; package Seqs is new Ada.Containers.Functional_Vectors (Index, Resource); use Seqs; function Create return Sequence with Post => (for all K in 1 .. Last (Create'Result) => Get (Create'Result, K) = K) is S : Sequence; begin for K in 1 .. 42 loop S := Add (S, K); pragma Loop_Invariant (Integer (Length (S)) = K); pragma Loop_Invariant (for all J in 1 .. K => Get (S, J) = J); end loop; return S; end Create; begin null; end Example_10;

This code is correct.