If the current version does not build, please use git commit "ea74065" which is the commit for the ITP submission.

-----------------------------

How to build?

Step 1: build VST. In the parent folder of this folder, do "make depend; make floyd".
Step 2: build this demo. In the child folder "wand_demo" of this folder, do "make depend; make". It will also build part of VFA that we use.

------------------------------

Where are all proofs?

1. wandQ_frame.v wand_frame.v: soundness of wandQ_frame and wand_frame rules.

2. bst_lemmas.v:
2.1. The definitions and properties of tree_rep, treebox_rep, Map_rep and Mapbox_rep. They are not in any module.
2.2. Module PartialTree_WandQFrame_Func_Hole: definitions and properties of partialT.
2.3. Module PartialTreeboxRep_WandQFrame_Func_Hole: definitions and properties of partial_treebox_rep.
2.4. Module PartialTreeRep_WandQFrame_Func_Hole: definitions and properties of partial_tree_rep.
2.5. Other modules: alternative definitions and proofs of partial_treebox_rep, for comparison purpose.

3. spec_bst.v: specifications of BST insert, lookup, delete.

4. verif_bst.v:
4.1. Module insert_by_WandQFrame_Func_Hole: our main theorem---the proof of insert.
4.2. Other modules: alternative proofs using alternative definitions of partial_treebox_rep, for comparison purpose.

5. verif_bst_other.v: the proof of BST lookup and delete.

6. lst_lemmas: the definition and proofs (and alternative definitions and proofs) of list_rep, lseg etc.

7. verif_list: the proof (and alternative proofs) of linked list append.

----------------------

Where are automated tactics? Where are their applications?

1. sep_absorb (mentioned in the paper) is in wandQ_frame_tactic.v.

2. solve_wandQ [sp] is the tactic for proving both elimination rules and vertical combination rules.
2.1. It uses sep_absorb.
2.2. [sp] is the name of separation logic predicate which is defined by quantified wand expression, e.g. [lseg].
2.3. This tactic is also defined in wandQ_frame_tactic.v.

3. Toy demos: Module solve_wandQ_playground in wandQ_frame_tactic.v.

4. lseg_lseg_proof_by_tactic, list_lseg_proof_by_tactic in list_lemmas.v.

5. partialT_rep_partialT_rep_proof_by_tactic, rep_partialT_rep_proof_by_tactic in bst_lemmas.v.

6.1. The majority of our proofs is not done by this automated tactic [solve_wandQ].
6.2. We put a comment on line 516 indicating that we can also use automated tactics there. At places like this, we just choose not to use [solve_wandQ] but to illustrate the usage of [wandQ_frame] rules.
6.3. Even for those several application examples, we have already proved them manually. We redo them by [solve_wandQ] in order to show that our tactic can complete the proof.

----------------------

Explanation for Print Assumptions.

The "Print Assumptions" command will output a long list which can be classified into 4 category:

1. Extensionality Axioms, e.g. functional extensinoality, propositional extensionality ((P <-> Q) -> (P = Q)).

2. Axioms of real numbers. They come from Coq's standard library of Real. And CompCert's floating point number reasoning uses that.

3. Axioms of Hoare logic rules for C. They actually not Coq axioms; they are Coq theorems which have been proved sound. It is a Coq's bug related to the interaction between "Print Assumptions" and Coq's modular system.

4. Exercises in VFA, which are admitted proofs. Their proofs appear in VFA's internal development but not in released versions.