Formalization of SPARK2014 in Coq Proof Assistant

===========
 Notes:
===========
it’s compiled with Coq8.5 version
run: ./makegen  will generate Makefile,
within Makefile, replace the following two lines:
COQLIBS?=\
  -R "." Top\
  -I "."
COQDOCLIBS?=\
  -R "." Top

with: 

COQLIBS?=-I "." 
COQDOCLIBS?= 

============
     Overview
============
In Coq Proof Assistant, we did a semantical formalization for a 
subset of SPARK2014 language, including array, record and nested
procedures; Besides, we also define a formal semantics for the 
run-time-checks-flagged SPARK2014 language; and prove that 
the run-time check flags generated by our formalized run-time checks
generator are correct with respect to the SPARK formal semantics; 
The formally proved correct run-time check flags can then be used to
verify the run-time check flags generated by Gnat front end;
In the end, we have formalized some simple optimizations for run-time 
checks and prove that any SPARK program will evaluate to the same
result before and after the run-time checks optimizations;


============
  Coq Source Code
============

- CpdtTactics.v
   it provides the tactic called "smack" which is implemented by 
   Adam Chlipala in his "Certified Programming with Dependent Types" 
   book; the "smack" tactic is powerful and can save a lot of time and 
   proof effort during Coq proof;

- LibTactics.v
   it contains a set of tactics that extends the set of builtin 
   tactics provided with the standard distribution of Coq. 
   It intends to overcome a number of limitations of the 
   standard set of tactics, and thereby to help user to write 
   shorter and more robust scripts;

- more_list.v
   it provides some list operations, e.g. list split, and 
   corresponding lemmas;

- language_basics.v
- language_template.v
- language.v
- language_flagged.v
   * language_basics.v defines some basic data types and operators 
     and literals that are used to define the SPARK 2014 AST syntax;
   * language_template.v defines a template for SPARK 2014 AST
     syntax; run the script program "languagegen" will generate
     language.v and language_flagged.v automatically;
   * language.v defines the SPARK 2014 AST syntax, which is used to
      to formalize SPARK 2014 reference semantics;
   * language_flagged.v is the same as language.v  except that each 
     AST node is extended with a set of run-time check flags; this 
     check-flagged language is used to represent the SPARK ASTs
     that are generated by Gnat front end, which inserts run-time
     check flags to SPARK AST during its static semantical analysis;
   * both language_basics.v and language_template.v can be generated
      automatically by our Sireum Jago translation tool developed at
      K-State, which translates gnat2xml-generated Ada XML Schema 
      to (inductive) type definitions in Coq; 
      (Sireum Jago is illustrated in following sections)

- checks.v
- checks_generator.v
- checks_comparison.v
   * checks.v defines a subset of run-time check flags that are
     required by our formalized SPARK2014 subset, including 
     division check, overflow check and range check; it also
     defines some comparison functions for run-time check flags;
   * checks_generator.v defines run-time check flags generator 
     according to the run-time check flags generation rules defined
     in Ada/SPARK reference manual; the check generator is formalized
     in both inducitive check generation rules and functional check
     generation program and prove them to be semantic equivalent;
   * checks_comparison.v defines comparison functions for two 
     run-time checks-flagged SPARK ASTs, and return all AST nodes
     where their run-time check flags are mismatching; furthermore, 
     they can also be mapped back to the SPARK source code to denote 
     where the run-time checks are misssing or misplaced;
     this can be used to compare the Gnat-generated SPARK AST against
     our formally verified check-flagged SPARK AST, and report any 
     missing or misplaced run-time check flags inserted by Gnat front
     end;

- values.v
   it defines values and corresponding operations that are used to define the 
   SPARK semantics;

- environment.v
   it defines store and stack as memory model for evaluating SPARK
   programs, including some basic store and stack operations and
   useful lemmas;

- symboltable_module.v
- symboltable.v
   * symboltable_module.v defines a template for symbol table and 
     its lookup and update operations; the symbol table stores
     procedure declarations and type declarations;
   * symboltable.v defines the symbol table and its corresponding
     operations for SPARK programs (in language.v) and the symbol 
     table for check-flagged SPARK programs (in language_flagged.v);
  
- semantics.v
- semantics_flagged.v
   * semantics.v defines the formal semantics for SPARK2014 Language 
     (defined in language.v), which is used as SPARK reference semantics; 
   * semantics_flagged.v defines the formal semantics for checks-flagged
     SPARK2014 Language (defined inlanguage_flagged.v);

- checks_soundness.v
   it proves that run-time check flags generated by checks generator 
   are correct with respect to the SPARK reference semantics; so they 
   can be used to verify the correctness of run-time check flags 
   generated by Gnat front end;

- checks_optimization.v
   it implements some simple run-time checks optimization for linear operations;
   
- well_typed.v
- well_check_flagged.v
   * well_typed.v defines the well-typed stack, where the value of
     each variable in the stack should be a value of the type of the 
     varialbe itself, and it defines the well-typedness of the SPARK
     program , where the each AST node should be well-typed;
   * well_check_flagged.v specifies that the checks-flagged SPARK 
     program should be annotated with correct run-time check flags;
   * both well_typed.v and well_check_flagged.v are used as 
     constraint for SPARK program to prove the soundness of 
     run-time checks optimization;

- checks_optimization_soundness.v
   * it proves that the evaluation of SPARK programs should be the
     same before and after the run-time checks optimization;


====================
  Compile/Document Coq Files
====================

- makegen
   it can be editted and executed (by running "makegen" in terminal)
   to generate the Makefile and then run "make" in terminal to compile 
   the above Coq source files;

- htmlgen
   it can be editted and executed (by running "htmlgen" in terminal) 
   to generate html files for the above Coq source files;

=================
  Sireum Jago Translators
=================
- Sireum Jago: which performs two kinds of translation: 
   * type translation, which translates gnat2xml-generated XML Schema 
      to (inductive) type definitions in Coq
   * program translation, which translates SPARK programs from 
     gnat2xml-generated XML AST to Coq AST;


=================
   Getting Started
=================

1. Download and install Sireum (Stable version) following instructions
   at : http://www.sireum.org/software.html

2. Run Sireum to test SPARK Type and Program Translation

In terminal:
2.1. command: "sireum bakar type -t Coq" 
       will translate SPARK XML Schema into SPARK type definition in Coq; 

2.2. command: "sireum bakar program -p Coq <SPARK_Source_File> [<Destination_File>]" 
       will translate the SPARK program into Coq AST;

3. command "./test_demo coq_ast_source_file_name target_file_name.v"
       will verify the run-time check flags generated by Gnat front
       end against our formally verified run-time check flags and
       report any mismatching run-time check flags and map them back
       to SPARK source programs;
    * test_demo is a script program (put under the same directory as
       the other Coq source files) to do the run-time checks;
       comparison and mapping back the error to SPARK source code;
    * coq_ast_source_file_name is a file contain the Coq AST generated
       in step 2.2;
    * target_file_name can be any target coq file name;


========================
  Limitations of SPARK2014 Subset
========================

- not support for function and function call now
- not support for "return" statement
- no support for “or_else_short_circuit” or “and_then_short_circuit” operators
- no support for string
- ...