Merge from LFSC (#26)

* Showing models as coq counter examples in tactic without constructing coq terms

* also read models when calling cvc4 with a file (deactivated because cvc4 crashes)

* Show counter examples with variables in the order they are quantified in the Coq goal

* Circumvent issue with ocamldep

* fix issue with dependencies

* fix issue with dependencies

* Translation and OCaml support for extract, zero_extend, sign_extend

* Show run times of components

* print time on stdout instead

* Tests now work with new version (master) of CVC4

* fix small printing issue

* look for date on mac os x

* proof of valid_check_bbShl: some cases to prove.

* full proof of "left shift checker".

*  full proof of "rigth shift checker".

* Support translation of terms bvlshr, bvshl but LFSC rules do not exists at the moment
Bug fix for bitvector extract (inverted arguments)

* Typo

* More modularity on the format of traces depending on the version of coq

* More straightforward definitions in Int63Native_standard

* Use the Int31 library with coq-8.5

* Use the most efficient operations of Int31

* Improved performance with coq-8.5

* Uniform treatment of sat and smt tactics

* Hopefully solved the problem with universes for the tactic

* Updated the installation instructions

* Holes for unsupported bit blasting rules

* Cherry-picking from smtcoq/smtcoq

* bug fix hole for bitblast

* Predefined arrays are not required anymore

* fix issue with coq bbT and bitof construction from ocaml

* bug fix in smtAtom for uninterpreted functions
fix verit test file

* fix issue with smtlib2 extract parsing

* It looks like we still need the PArray function instances for some examples (see vmcai_bytes.smt2)

* Solver specific reification:
Each solver has a list of supported theories which is passed to Atom.of_coq, this function creates uninterpreted functions / sorts for unsupported features.

* show counter-examples with const_farray instead of const for constant array definitions

* Vernacular commands to debug checkers.
Verit/Lfsc_Checker_Debug will always fail, reporting the first proof step of the certificate that failed be checked

* Update INSTALL.md

* show smtcoq proof when converting

* (Hopefully) repared the universes problems

* Corrected a bug with holes in proofs

* scripts for tests:
create a folder "work" under "lfsc/tests/", locate the benchmarks there.
create a folder "results" under "lfsc/tests/work/" in which you'll find the results of ./cvc4tocoq.

* make sure to give correct path for your benchs...

* Checker for array extensionality modulo symmetry of equality

* fix oversight with bitvectors larger than 63 bits

* some printing functions for smt2 ast

* handle smtlib2 files with more complicated equivalence with (= ... )

* revert: ./cvc4tocoq does not output lfsc proofs...

* bug fix one input was ignored

* Don't show verit translation of LFSC proof if environment variable DONTSHOWVERIT is set
(e.g. put export DONTSHOWVERIT="" in your .bashrc or .bashprofile)

* Also sort names of introduced variables when showing counter-example

* input files for which SMTCoq retuns false.

* input files for which SMTCoq retuns false.

* use debug checker for debug file

* More efficient debug checker

* better approximate number of failing step of certificate in debug checker

* fix mistake in ml4

* very first attempt to support goals in Prop

* bvs: comparison predicates in Prop and their <-> proofs with the ones in bool
farrays: equality predicate in Prop and its <-> proof with the one in bool.

* unit, Bool, Z, Pos: comparison and equality predicates in Prop.

* a typo fixed.

* an example of array equality in  Prop (converted into Bool by hand)...
TODO: enhance the search space of cvc4 tactic.

* first version of cvc4' tactic: "solves" the goals in Prop.
WARNING: supports only bv and array goals and might not be complete
TODO: add support for lia goals

* cvc4' support for lia
WARNING: might not be complete!

* small fix in cvc4' and some variations of examples

* small fix + support for goals in Bool and Bool = true + use of solve tactical
WARNING: does not support UF and INT63 goals in Prop

* cvc4': better arrangement

* cvc4': Prop2Bool by context search...

* cvc4': solve tactial added -> do not modify unsolved goals.

* developer documentation for the smtcoq repo

* cvc4': rudimentary support for uninterpreted function goals in Prop.

* cvc4': support for goals with Leibniz equality...
WARNING: necessary use of "Grab Existential Variables." to instantiate variable types for farrays!

* cvc4': Z.lt adapted + better support from verit...

* cvc4': support for Z.le, Z.ge, Z.gt.

* Try arrays with default value (with a constructor for constant arrays), but extensionality is not provable

* cvc4': support for equality over uninterpreted types

* lfsc demo: goals in Coq's Prop.

* lfsc demo: goals in Bool.

* Fix issue with existential variables generated by prop2bool.
- prop2bool tactic exported by SMTCoq
- remove useless stuff

* update usage and installation instructions

* Update INSTALL.md

* highlighting

* the tactic: bool2prop.

* clean up

* the tactic smt: very first version.

* smt: return unsolved goals in Prop.

* Show when a certificate cannot be checked when running the tactic instead of at Qed

* Tactic improvements
- Handle negation/True/False in prop/bool conversions tactic.
- Remove alias for farray (this caused problem for matching on this type in tactics).
- Tactic `smt` that combines cvc4 and veriT.
- return subgoals in prop

* test change header

* smt: support for negated goals + some reorganization.

* conflicts resolved + some reorganization.

* a way to solve the issue with ambiguous coercions.

* reorganization.

* small change.

* another small change.

* developer documentation of the tactics.

* developer guide: some improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* pass correct environment for conversion + better error messages

* cleaning

* ReflectFacts added.

* re-organizing developers' guide.

* re-organizing developers' guide.

* re-organizing developers' guide.

* removing unused maps.

* headers.

* artifact readme getting started...

* first attempt

* second...

* third...

* 4th...

* 5th...

* 6th...

* 7th...

* 8th...

* 9th...

* 10th...

* 11th...

* 12th...

* 13th...

* 14th...

* 15th...

* 16th...

* 17th...

* Update artifact.md

Use links to lfsc repository like in the paper

* 18th...

* 19th...

* 20th...

* 21st...

* 22nd...

* 23rd...

* 24th...

* 25th...

* 26th...

* 27th...

* 28th...

* Update artifact.md

Small reorganization

* minor edits

* More minor edits

* revised description of tactics

* Final pass

* typo

* name changed: artifact-readme.md

* file added...

* passwd chaged...

* links...

* removal

* performance statement...

* typos...

* the link to the artifact image updated...

* suggestions by Guy...

* aux files removed...

* clean-up...

* clean-up...

* some small changes...

* small fix...

* additional information on newly created files after running cvc4tocoq script...

* some small fix...

* another small fix...

* typo...

* small fix...

* another small fix...

* fix...

* link to the artifact image...

* We do not want to force vm_cast for the Theorem commands

* no_check variants of the tactics

* TODO: a veriT test does not work anymore

* Compiles with both versions of Coq

* Test of the tactics in real conditions

* Comment on this case study

* an example for the FroCoS paper.

* Fix smt tactic that doesn't return cvc4's subgoals

* readme modifications

* readme modifications 2

* small typo in readme.

* small changes in readme.

* small changes in readme.

* typo in readme.

* Sync with https://github.com/LFSC/smtcoq

* Port to Coq 8.6

* README

* README

* INSTALL

* Missing file

* Yves' proposition for installation instructions

* Updated link to CVC4

* Compiles again with native-coq

* Compiles with both versions of Coq

* Command to bypass typechecking when generating a zchaff theorem

* Solved bug on cuts from Hole

* Counter-models for uninterpreted sorts (improves issue #13)

* OCaml version note (#15)

* update .gitignore

* needs OCaml 4.04.0

* Solving merge issues (under progress)

* Make SmtBtype compile

* Compilation of SmtForm under progress

* Make SmtForm compile

* Make SmtCertif compile

* Make SmtTrace compile

* Make SatAtom compile

* Make smtAtom compile

* Make CnfParser compile

* Make Zchaff compile

* Make VeritSyntax compile

* Make VeritParser compile

* Make lfsc/tosmtcoq compile

* Make smtlib2_genconstr compile

* smtCommand under progress

* smtCommands and verit compile again

* lfsc compiles

* ml4 compiles

* Everything compiles

* All ZChaff unit tests and most verit unit tests (but taut5 and un_menteur) go through

* Most LFSC tests ok; some fail due to the problem of verit; a few fail due to an error "Not_found" to investigate

* Authors and headings

* Compiles with native-coq

* Typo

1 files changed, 1272 insertions, 0 deletions

diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
new file mode 100644
index 0000000..dd1a65f
--- /dev/null
+++ b/src/array/Array_checker.v
@@ -0,0 +1,1272 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Import Bool List Int63 PArray SMT_classes.
+Require Import Misc State SMT_terms FArray.
+
+Import Form.
+Import Atom.
+
+Local Open Scope array_scope.
+Local Open Scope int63_scope.
+
+Section certif.
+
+  Variable t_form : PArray.array Form.form.
+  Variable t_atom : PArray.array Atom.atom.
+
+  Local Notation get_atom := (PArray.get t_atom) (only parsing).
+  Local Notation get_form := (PArray.get t_form) (only parsing).
+
+
+  Definition check_roweq lres :=
+    if Lit.is_pos lres then
+      match get_form (Lit.blit lres) with
+      | Fatom a =>
+        match get_atom a with
+        | Abop (BO_eq te) xa v =>
+          match get_atom xa with
+          | Abop (BO_select ti1 te1) sa i =>
+            match get_atom sa with
+            | Atop (TO_store ti2 te2) fa j v2 =>
+              if Typ.eqb ti1 ti2 &&
+                 Typ.eqb te te1 && Typ.eqb te te2 &&
+                 (i == j) && (v == v2)
+              then lres::nil
+              else C._true
+            | _ => C._true
+            end
+          | _ => C._true
+          end
+        | _ => C._true
+        end
+      | _ => C._true
+      end
+    else C._true.
+
+
+  Definition store_of_me a b :=
+    match get_atom b with
+    | Atop (TO_store ti te) a' i _ =>
+      if (a' == a) then Some (ti, te, i) else None
+    | _ => None
+    end.
+ 
+  
+  Definition check_rowneq cl :=
+    match cl with
+    | leqij :: leqrow :: nil =>
+      if Lit.is_pos leqij && Lit.is_pos leqrow then
+        match get_form (Lit.blit leqij), get_form (Lit.blit leqrow) with
+        | Fatom eqij, Fatom eqrow =>
+          match get_atom eqij, get_atom eqrow with
+          | Abop (BO_eq ti) i j, Abop (BO_eq te) xa x =>
+            match get_atom xa, get_atom x with
+            | Abop (BO_select ti1 te1) sa j1, Abop (BO_select ti2 te2) sa2 j2 =>
+              if Typ.eqb ti ti1 && Typ.eqb ti ti2 &&
+                 Typ.eqb te te1 && Typ.eqb te te2 then
+                match store_of_me sa sa2, store_of_me sa2 sa with
+                | Some (ti3, te3, i1), None | None, Some (ti3, te3, i1) => 
+                  if Typ.eqb ti ti3 && Typ.eqb te te3 &&
+                     (((i1 == i) && (j1 == j) && (j2 == j)) ||
+                      ((i1 == j) && (j1 == i) && (j2 == i))) then
+                    cl
+                  else C._true
+                | _, _ => C._true
+                end
+              else C._true
+            | _, _ => C._true
+            end
+          | _, _ => C._true
+          end
+        | _, _ => C._true
+        end
+      else C._true
+    | _ => C._true
+    end.
+
+
+
+  Definition eq_sel_sym ti te a b sela selb :=
+    match get_atom sela, get_atom selb with
+    | Abop (BO_select ti1 te1) a' d1, Abop (BO_select ti2 te2) b' d2 =>
+      Typ.eqb ti ti1 && Typ.eqb ti ti2 &&
+      Typ.eqb te te1 && Typ.eqb te te2 &&
+      (a == a') && (b == b') && (d1 == d2) &&
+      match get_atom d1 with
+      | Abop (BO_diffarray ti3 te3) a3 b3 =>
+        Typ.eqb ti ti3 && Typ.eqb te te3 &&
+        (a3 == a) && (b3 == b)
+      | _ => false
+      end
+    | _, _ => false
+    end.
+  
+  
+  Definition check_ext lres :=
+    if Lit.is_pos lres then
+      match get_form (Lit.blit lres) with
+      | For args =>
+        if PArray.length args == 2 then
+          let l1 := args.[0] in
+          let l2 := args.[1] in
+          if Lit.is_pos l1 && negb (Lit.is_pos l2) then
+            match get_form (Lit.blit l1), get_form (Lit.blit l2) with
+            | Fatom eqa, Fatom eqsel =>
+              match get_atom eqa, get_atom eqsel with
+              | Abop (BO_eq (Typ.TFArray ti te)) a b, Abop (BO_eq te') sela selb => 
+                if Typ.eqb te te' && (eq_sel_sym ti te a b sela selb ||
+                                      eq_sel_sym ti te b a sela selb) then
+                  lres :: nil
+                else C._true
+              | _, _ => C._true
+              end
+            | _, _ => C._true
+            end
+          else C._true
+        else C._true
+      | _ => C._true
+      end
+    else C._true.
+
+
+  Section Correct.
+
+    Variables (t_i : array typ_compdec)
+              (t_func : array (Atom.tval t_i))
+              (ch_atom : Atom.check_atom t_atom)
+              (ch_form : Form.check_form t_form)
+              (wt_t_atom : Atom.wt t_i t_func t_atom).
+
+    Local Notation check_atom :=
+      (check_aux t_i t_func (get_type t_i t_func t_atom)).
+
+    Local Notation interp_form_hatom :=
+      (Atom.interp_form_hatom t_i t_func t_atom).
+
+    Local Notation interp_form_hatom_bv :=
+      (Atom.interp_form_hatom_bv t_i t_func t_atom).
+
+    Local Notation rho :=
+      (Form.interp_state_var interp_form_hatom interp_form_hatom_bv t_form).
+
+    Local Notation t_interp := (t_interp t_i t_func t_atom).
+
+    Local Notation interp_atom := (interp_aux t_i t_func (get t_interp)).
+
+    Let wf_t_atom : Atom.wf t_atom.
+    Proof. destruct (Atom.check_atom_correct _ ch_atom); auto. Qed.
+
+    Let def_t_atom : default t_atom = Atom.Acop Atom.CO_xH.
+    Proof. destruct (Atom.check_atom_correct _ ch_atom); auto. Qed.
+
+    Let def_t_form : default t_form = Form.Ftrue.
+    Proof.
+      destruct (Form.check_form_correct
+                  interp_form_hatom interp_form_hatom_bv _ ch_form) as [H _];
+        destruct H; auto.
+    Qed.
+
+    Let wf_t_form : Form.wf t_form.
+    Proof.
+      destruct (Form.check_form_correct
+                  interp_form_hatom interp_form_hatom_bv _ ch_form) as [H _];
+        destruct H; auto.
+    Qed.
+
+    Let wf_rho : Valuation.wf rho.
+    Proof.
+      destruct (Form.check_form_correct
+                  interp_form_hatom interp_form_hatom_bv _ ch_form); auto.
+    Qed.
+
+    Let rho_interp : forall x : int,
+        rho x = Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[ x]).
+    Proof. intros x;apply wf_interp_form;trivial. Qed.
+
+    Definition wf := PArray.forallbi lt_form t_form.
+
+    Hypothesis wf_t_i : wf.
+    Notation atom := int (only parsing).
+
+    
+    Lemma valid_check_roweq lres : C.valid rho (check_roweq lres).
+    Proof.
+      unfold check_roweq.
+      case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true.
+      case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
+      intros a Heq2.
+      case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
+      intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq3; try (intros; now apply C.interp_true).
+      case_eq (t_atom .[ a1]); try (intros; now apply C.interp_true).
+      intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq4; try (intros; now apply C.interp_true).
+      case_eq (t_atom .[ b1]); try (intros; now apply C.interp_true).
+      intros [ ] c1 c2 c3 Heq5.
+      (* roweq *)
+      - case_eq (Typ.eqb t0 t2 && Typ.eqb t t1 && 
+             Typ.eqb t t3 && (b2 == c2) && (a2 == c3)); simpl; intros Heq6; try (now apply C.interp_true).
+
+        unfold C.valid. simpl. rewrite orb_false_r.
+        unfold Lit.interp. rewrite Heq.
+        unfold Var.interp.
+        rewrite wf_interp_form; trivial. rewrite Heq2. simpl.
+
+        rewrite !andb_true_iff in Heq6.
+        destruct Heq6 as ((((Heq6a, Heq6b), Heq6c), Heq6d), Heq6e).
+
+        apply Typ.eqb_spec in Heq6a.
+        apply Typ.eqb_spec in Heq6b.
+        apply Typ.eqb_spec in Heq6c.
+        apply Int63Properties.eqb_spec in Heq6d.
+        apply Int63Properties.eqb_spec in Heq6e.
+
+        pose proof (rho_interp (Lit.blit lres)) as Hrho.
+        rewrite Heq2 in Hrho. simpl in Hrho.
+
+        generalize wt_t_atom. unfold Atom.wt. unfold is_true.
+        rewrite PArray.forallbi_spec;intros.
+
+        pose proof (H a). assert (a < PArray.length t_atom).
+        apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy.
+        specialize (H0 H1). simpl in H0.
+        rewrite Heq3 in H0. simpl in H0.
+        rewrite !andb_true_iff in H0. destruct H0. destruct H0.
+        unfold get_type' in H2, H3, H0. unfold v_type in H2, H3, H0.
+
+        case_eq (t_interp .[ a]).
+          intros v_typea v_vala Htia. rewrite Htia in H0.
+          case_eq v_typea; intros; rewrite H4 in H0; try now contradict H0.
+
+        case_eq (t_interp .[ a1]).
+          intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H3.
+        case_eq (t_interp .[ a2]).
+          intros v_typea2 v_vala2 Htia2. rewrite Htia2 in H2.
+        rewrite Atom.t_interp_wf in Htia; trivial.
+        rewrite Atom.t_interp_wf in Htia1; trivial.
+        rewrite Atom.t_interp_wf in Htia2; trivial.
+        rewrite Heq3 in Htia. simpl in Htia.
+        rewrite !Atom.t_interp_wf in Htia; trivial.
+        rewrite Htia1, Htia2 in Htia. simpl in Htia.
+
+        apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3.
+
+        generalize dependent v_vala1. generalize dependent v_vala2.
+        generalize dependent v_vala.
+
+        rewrite H2, H3, H4.
+        rewrite !Typ.cast_refl. intros. simpl in Htia.
+        unfold Bval in Htia.
+
+        specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t v_vala1 v_vala2) (v_vala)).
+        intros. specialize (H5 Htia).
+
+        pose proof (H a1). assert (a1 < PArray.length t_atom).
+        apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4. easy.
+        specialize (H6 H7). simpl in H6.
+        rewrite Heq4 in H6. simpl in H6.
+        rewrite !andb_true_iff in H6.
+        destruct H6 as ((H6a, H6b), H6c).
+        apply Typ.eqb_spec in H6a.
+        apply Typ.eqb_spec in H6b.
+        apply Typ.eqb_spec in H6c.
+
+        pose proof (H b1). assert (b1 < PArray.length t_atom).
+        apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq5. easy.
+        specialize (H6 H8). simpl in H6.
+        rewrite Heq5 in H6. simpl in H6.
+
+        rewrite !andb_true_iff in H6.
+        destruct H6 as (((H6d, H6e), H6f), H6h).
+        apply Typ.eqb_spec in H6e.
+        apply Typ.eqb_spec in H6f.
+        apply Typ.eqb_spec in H6h.
+
+        unfold get_type' in H6b, H6c, H6d.
+        unfold v_type in H6b, H6c, H6d.
+        case_eq (t_interp .[ b2]). 
+          intros v_typeb2 v_valb2 Htib2. rewrite Htib2 in H6c.
+        rewrite Atom.t_interp_wf in Htib2; trivial.
+        case_eq (t_interp .[ b1]). 
+          intros v_typeb1 v_valb1 Htib1. rewrite Htib1 in H6d.
+        rewrite Atom.t_interp_wf in Htib1; trivial.
+        rewrite <- Heq6d, <- Heq6e in *.
+
+        rewrite Heq5 in Htib1. simpl in Htib1.
+
+        generalize dependent v_valb2.
+
+        rewrite H6c. intros.
+        unfold Atom.interp_form_hatom, interp_hatom.
+        rewrite !Atom.t_interp_wf; trivial.
+        rewrite Heq3. simpl.
+        rewrite !Atom.t_interp_wf; trivial.
+        rewrite Heq4, Htia2. simpl.
+        rewrite !Atom.t_interp_wf; trivial.
+        rewrite Heq5, Htib2. simpl. 
+        rewrite Htib1. simpl.
+
+        rewrite Typ.cast_refl.
+        unfold apply_binop.
+        rewrite Typ.cast_refl.
+
+        case_eq (t_interp .[ b1]); intros.
+        pose proof H6.
+        rewrite H6 in H6b.
+        rewrite !Atom.t_interp_wf in H6; trivial.
+        rewrite Heq5 in H6.
+        simpl in H6. rewrite H6 in Htib1.
+        inversion Htib1.
+
+        generalize dependent v_val0.
+
+        rewrite H6b.
+        intros. rewrite Typ.cast_refl.
+        simpl.
+        unfold get_type' in H6a.
+        unfold v_type in H6a.
+        case_eq (t_interp .[ a1]).
+        intros.
+        rewrite H10 in H6a.
+        rewrite !Atom.t_interp_wf in H10; trivial.
+        rewrite H10 in Htia1.
+        inversion Htia1.
+        rewrite <- H6a in H14.
+
+        generalize dependent v_val0.
+
+        rewrite H14.
+        intros.
+        rewrite Typ.cast_refl.
+        simpl.
+
+        unfold apply_terop in H6.
+        unfold get_type', v_type in H6e, H6f, H6h.
+        case_eq ( t_interp .[ c1]); intros.
+        rewrite H13 in H6e.
+        rewrite H13 in H6.
+        case_eq (t_interp .[ b2]); intros.
+        rewrite H16 in H6f.
+        rewrite H16 in H6.
+        case_eq (t_interp .[ a2]); intros.
+        rewrite H17 in H6h.
+        rewrite H17 in H6.
+
+        generalize dependent v_val2. generalize dependent v_val3.
+        generalize dependent v_val4.
+
+        rewrite H6e, H6f, H6h.
+        rewrite !Typ.cast_refl.
+        intros.
+        unfold Bval in H6.
+
+        rewrite <- H11 in H6d.
+        rewrite H6b in H6d.
+        rewrite andb_true_iff in H6d.
+        destruct H6d as (H6d1, H6d2).
+        apply Typ.eqb_spec in H6d1.
+        apply Typ.eqb_spec in H6d2.
+
+        generalize dependent v_val2. generalize dependent v_val3.
+        generalize dependent v_val4.
+
+        rewrite H6d1, H6d2, H14.
+        intros.
+        specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t) 
+        (store v_val2 v_val3 v_val4) (v_val0)).
+        intros. specialize (H18 H6).
+        rewrite <- H18.
+
+        rewrite !Atom.t_interp_wf in H16; trivial.
+        rewrite H16 in Htib2.
+        specialize (Atom.Bval_inj2 t_i t0 v_val3 v_valb2).
+        intros. specialize (H19 Htib2).
+        rewrite <- H19.
+
+        rewrite !Atom.t_interp_wf in H17; trivial.
+        rewrite H17 in Htia2.
+        specialize (Atom.Bval_inj2 t_i t v_val4 v_vala2).
+        intros. specialize (H20 Htia2).
+        rewrite <- H20.
+        apply Typ.i_eqb_spec.
+        apply (read_over_write (elt_dec:=(EqbToDecType _ (@Eqb _ _)))).
+    Qed.
+
+
+    
+    Lemma valid_check_rowneq cl : C.valid rho (check_rowneq cl).
+    Proof.
+        unfold check_rowneq.
+        case_eq (cl); [ intros | intros i l ]; simpl; try now apply C.interp_true.
+        case_eq (l); [ intros | intros j xsl ]; simpl; try now apply C.interp_true.
+        case_eq (xsl); intros; simpl; try now apply C.interp_true.
+        case_eq (Lit.is_pos i); intro Heq; simpl; try now apply C.interp_true.
+        case_eq (Lit.is_pos j); intro Heq2; simpl; try now apply C.interp_true.
+        case_eq (t_form .[ Lit.blit i]); try (intros; now apply C.interp_true).
+        intros a Heq3.
+        case_eq (t_form .[ Lit.blit j]); try (intros; now apply C.interp_true).
+        intros b Heq4.
+        case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
+        intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] a1 a2 Heq5; try (intros; now apply C.interp_true).
+        case_eq (t_atom .[ b]); try (intros; now apply C.interp_true).
+        intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq6; try (intros; now apply C.interp_true).
+        case_eq (t_atom .[ b1]); try (intros; now apply C.interp_true).
+        intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq7; try (intros; now apply C.interp_true).
+        case_eq (t_atom .[ b2]); try (intros; now apply C.interp_true).
+        intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq8; try (intros; now apply C.interp_true).
+        case_eq (Typ.eqb t t1 && Typ.eqb t t3 && Typ.eqb t0 t2 && Typ.eqb t0 t4); 
+          try (intros; now apply C.interp_true). intros Heq9.
+
+
+        rewrite !andb_true_iff in Heq9.
+        destruct Heq9 as (((Heq9a, Heq9b), Heq9c), Heq9d).
+
+        apply Typ.eqb_spec in Heq9a.
+        apply Typ.eqb_spec in Heq9b.
+        apply Typ.eqb_spec in Heq9c.
+        apply Typ.eqb_spec in Heq9d.
+        subst t1 t2 t3 t4.
+
+        generalize wt_t_atom. unfold Atom.wt. unfold is_true.
+        rewrite PArray.forallbi_spec;intros.
+
+        assert (H15: b1 < PArray.length t_atom).
+        apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq7. discriminate.
+        assert (H20: b2 < PArray.length t_atom).
+        apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq8. discriminate.
+        assert (H9: b < PArray.length t_atom).
+        apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. discriminate.
+        assert (H3: a < PArray.length t_atom).
+        apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq5. discriminate.
+
+
+        apply H2 in H15.
+        apply H2 in H20.
+        apply H2 in H3.
+        apply H2 in H9.
+
+        rewrite Heq7 in H15.
+        rewrite Heq8 in H20.
+        rewrite Heq6 in H9.
+        rewrite Heq5 in H3.
+
+        simpl in H15, H20, H3, H9.
+        
+        rewrite !andb_true_iff in H15, H20, H3, H9.
+
+        destruct H3 as ((H3, H6), H5).
+        destruct H9 as ((H9, H12), H11).
+        destruct H15 as ((H15, H18), H17).
+        destruct H20 as ((H20, H23), H22).
+        unfold get_type', v_type in H3, H5, H6, H9, H11, H12, H15, H17, H18, H20, H22, H23.
+
+        
+        case_eq (t_interp .[ a]).
+          intros v_typea v_vala Htia. rewrite Htia in H3.
+          case_eq v_typea; intros; rewrite H4 in H3; try now contradict H3.
+
+        case_eq (t_interp .[ a1]).
+          intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H6.
+        case_eq (t_interp .[ a2]).
+            intros v_typea2 v_vala2 Htia2. rewrite Htia2 in H5.
+        rewrite Atom.t_interp_wf in Htia, Htia1, Htia2; trivial.
+        rewrite Heq5 in Htia. simpl in Htia.
+        rewrite !Atom.t_interp_wf in Htia; trivial.
+        rewrite Htia1, Htia2 in Htia. simpl in Htia.
+
+        apply Typ.eqb_spec in H5. apply Typ.eqb_spec in H6.
+
+        generalize dependent v_vala1. generalize dependent v_vala2.
+        generalize dependent v_vala.
+        rewrite H5, H6, H4.
+        rewrite !Typ.cast_refl. intros. simpl in Htia.
+        unfold Bval in Htia.
+
+        specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t v_vala1 v_vala2) (v_vala)).
+        intros H8. specialize (H8 Htia).
+
+        case_eq (t_interp .[ b]).
+          intros v_typeb v_valb Htib. rewrite Htib in H9;
+          case_eq v_typeb; intros; rewrite H7 in H9; try now contradict H9.
+
+        case_eq (t_interp .[ b1]).
+          intros v_typeb1 v_valb1 Htib1. rewrite Htib1 in H12.
+        case_eq (t_interp .[ b2]).
+            intros v_typeb2 v_valb2 Htib2. rewrite Htib2 in H11.
+        rewrite Atom.t_interp_wf in Htib, Htib1, Htib2; trivial.
+        rewrite Heq6 in Htib. simpl in Htib.
+        rewrite !Atom.t_interp_wf in Htib; trivial.
+        rewrite Htib1, Htib2 in Htib. simpl in Htib.
+
+        apply Typ.eqb_spec in H11. apply Typ.eqb_spec in H12.
+
+
+        generalize dependent v_valb1. generalize dependent v_valb2.
+        generalize dependent v_valb.
+        rewrite H11, H12, H7.
+        rewrite !Typ.cast_refl. intros. simpl in Htib.
+        unfold Bval in Htib.
+
+        specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t0 v_valb1 v_valb2) (v_valb)).
+        intros H14. specialize (H14 Htib).
+
+       case_eq (t_interp .[ b1]).
+          intros v_typeb1' v_valb1' Htib1'. rewrite Htib1' in H15.
+
+        case_eq (t_interp .[ c1]).
+          intros v_typec1 v_valc1 Htic1. rewrite Htic1 in H18.
+        case_eq (t_interp .[ c2]).
+            pose proof Htib1' as Htib1''.
+            intros v_typec2 v_valc2 Htic2. rewrite Htic2 in H17.
+            pose proof Htic2 as Htic2''.
+        rewrite Atom.t_interp_wf in Htib1', Htic1, Htic2; trivial.
+        rewrite Heq7 in Htib1'. simpl in Htib1'.
+        rewrite !Atom.t_interp_wf in Htib1'; trivial.
+        rewrite Htic1, Htic2 in Htib1'. simpl in Htib1'.
+
+        apply Typ.eqb_spec in H17. apply Typ.eqb_spec in H18.
+        apply Typ.eqb_spec in H15. 
+
+        generalize dependent v_valc1. generalize dependent v_valc2.
+        generalize dependent v_valb1'.
+        rewrite H17, H18.
+        rewrite !Typ.cast_refl. intros. simpl in Htib1'.
+        unfold Bval in Htib1'.
+
+
+        generalize dependent v_valc1. generalize dependent v_valc2.
+        generalize dependent v_valb1'.
+
+        rewrite H15. intros.
+        specialize (Atom.Bval_inj2 t_i (v_typeb1') (select v_valc1 v_valc2) (v_valb1')).
+        intro H19. specialize (H19 Htib1').
+
+        (* b2 *)
+       case_eq (t_interp .[ b2]).
+          intros v_typeb2' v_valb2' Htib2'. rewrite Htib2' in H20.
+
+        case_eq (t_interp .[ d1]).
+          intros v_typed1 v_vald1 Htid1. rewrite Htid1 in H23.
+        case_eq (t_interp .[ d2]).
+            pose proof Htib2' as Htib2''.
+            intros v_typed2 v_vald2 Htid2. rewrite Htid2 in H22.
+        rewrite Atom.t_interp_wf in Htib2', Htid1, Htid2; trivial.
+        rewrite Heq8 in Htib2'. simpl in Htib2'.
+        rewrite !Atom.t_interp_wf in Htib2'; trivial.
+        rewrite Htid1, Htid2 in Htib2'. simpl in Htib2'.
+
+        apply Typ.eqb_spec in H22. apply Typ.eqb_spec in H23.
+        apply Typ.eqb_spec in H20. 
+
+        generalize dependent v_vald1. generalize dependent v_vald2.
+        generalize dependent v_valb2'.
+        rewrite H22, H23.
+        rewrite !Typ.cast_refl. intros. simpl in Htib2'.
+        unfold Bval in Htib2'.
+
+
+        generalize dependent v_vald1. generalize dependent v_vald2.
+        generalize dependent v_valb2'.
+
+        rewrite H20. intros.
+        specialize (Atom.Bval_inj2 t_i (v_typeb2') (select v_vald1 v_vald2) (v_valb2')).
+        intro H24. specialize (H24 Htib2').
+
+        
+        
+        case_eq (store_of_me c1 d1);
+          case_eq (store_of_me d1 c1);
+          try (intros; try(destruct p0, p0); now apply C.interp_true).
+        
+        - unfold store_of_me.
+          intro HT1. clear HT1.
+          case_eq (t_atom .[ d1]); try discriminate.
+          intros [ t5 t6 ] e1 e2 e3 Heq10 [[ti3 te3] i1].
+          case_eq (e1 == c1); try discriminate. intros Heq11c.
+          intro HT.
+          injection HT. intros. subst i1 te3 ti3. clear HT.
+
+          case_eq (
+              Typ.eqb t t5 && Typ.eqb v_typeb1' t6 &&
+                      ((e2 == a1) && (c2 == a2) && (d2 == a2) || (e2 == a2) && (c2 == a1) && (d2 == a1)));
+            simpl; intros Heq11; try (now apply C.interp_true).
+
+          unfold C.valid. simpl. rewrite orb_false_r.
+
+          case_eq (Lit.interp rho i). intros isit.
+          easy. intros isif. rewrite orb_false_l.
+          specialize (rho_interp ( Lit.blit i)).
+          rewrite Heq3 in rho_interp.
+          simpl in rho_interp.
+          unfold Lit.interp in isif.
+          rewrite Heq in isif. unfold Var.interp in isif.
+          rewrite rho_interp in isif.
+          unfold Atom.interp_form_hatom, interp_hatom in isif.
+          rewrite Atom.t_interp_wf in isif; trivial.
+          rewrite Heq5 in isif.
+          simpl in isif.
+          unfold interp_bool in isif.
+
+          unfold Lit.interp. rewrite Heq2.
+          unfold Var.interp.
+          rewrite !wf_interp_form; trivial. rewrite Heq4. simpl.
+
+          rewrite !andb_true_iff in Heq11.
+          destruct Heq11 as ((Heq11a, Heq11b), Heq11d).
+          rewrite !orb_true_iff in Heq11d.
+
+          apply Typ.eqb_spec in Heq11a.
+          apply Typ.eqb_spec in Heq11b.
+          apply Int63Properties.eqb_spec in Heq11c.
+          rewrite !andb_true_iff in Heq11d.
+          rewrite !Int63Properties.eqb_spec in Heq11d.
+
+
+          rewrite !Atom.t_interp_wf in isif; trivial.
+          rewrite Htia1, Htia2 in isif. simpl in isif.
+          unfold Bval in isif.
+
+
+          assert (H25: d1 < PArray.length t_atom).
+          apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq10. discriminate.
+          apply H2 in H25.
+          rewrite Heq10 in H25.
+          simpl in H25.
+          rewrite !andb_true_iff in H25.
+          destruct H25 as (((H25, H29), H28), H27).
+          unfold get_type', v_type in H25, H27, H28, H29.
+
+          case_eq (t_interp .[ d1]).
+          intros v_typed1' v_vald1' Htid1'. rewrite Htid1' in H25.
+          case_eq v_typed1'; intros; rewrite H10 in H25; try now contradict H25.
+          rewrite andb_true_iff in H25; destruct H25 as (H25a, H25b).
+
+          case_eq (t_interp .[ e1]).
+          intros v_typee1 v_vale1 Htie1. rewrite Htie1 in H29.
+          case_eq (t_interp .[ e2]).
+          intros v_typee2 v_vale2 Htie2. rewrite Htie2 in H28.
+          case_eq (t_interp .[ e3]).
+          intros v_typee3 v_vale3 Htie3. rewrite Htie3 in H27.
+          pose proof Htid1' as Htid1''.
+          rewrite Atom.t_interp_wf in Htid1', Htie1, Htie2, Htie3; trivial.
+          rewrite Heq10 in Htid1'. simpl in Htid1'.
+          rewrite !Atom.t_interp_wf in Htid1'; trivial.
+          rewrite Htie1, Htie2, Htie3 in Htid1'. simpl in Htid1'.
+
+          apply Typ.eqb_spec in H25a. apply Typ.eqb_spec in H25b.
+          apply Typ.eqb_spec in H27.  apply Typ.eqb_spec in H28.
+          apply Typ.eqb_spec in H29.
+
+          generalize dependent v_vale1. generalize dependent v_vale2.
+          generalize dependent v_vale3. generalize dependent v_vald1'.
+          rewrite H27, H28, H29.
+          rewrite !Typ.cast_refl. intros. simpl in Htid1'.
+          unfold Bval in Htid1'.
+
+
+          generalize dependent v_vale1. generalize dependent v_vale2.
+          generalize dependent v_vale3. generalize dependent v_vald1'.
+
+          rewrite H25a, H25b, H10. intros.
+          specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2)
+                                     (store v_vale1 v_vale2 v_vale3) (v_vald1')).
+          intro H25. specialize (H25 Htid1').
+          
+          unfold Atom.interp_form_hatom, interp_hatom.
+          rewrite !Atom.t_interp_wf; trivial.
+          rewrite Heq6. simpl.
+          rewrite !Atom.t_interp_wf; trivial.
+          rewrite Heq7, Heq8. simpl.
+          rewrite !Atom.t_interp_wf; trivial.
+
+          rewrite Htic1, Htic2, Htid1, Htid2.
+          subst. intros. simpl.
+          rewrite !Typ.cast_refl.
+          unfold apply_binop.
+          unfold Bval.
+          rewrite !Atom.t_interp_wf in Htib1''; trivial.
+          rewrite Htib1 in Htib1''.
+          inversion Htib1''.
+          rewrite !Atom.t_interp_wf in Htib2''; trivial.
+          rewrite Htib2 in Htib2''.
+          inversion Htib2''.
+
+          rewrite !Typ.cast_refl.
+
+          unfold interp_bool. rewrite Typ.cast_refl.
+          apply Typ.i_eqb_spec.
+
+          rewrite !Atom.t_interp_wf in Htid1''; trivial.
+          rewrite Htid1 in Htid1''.
+          inversion Htid1''.
+
+          subst.
+          rewrite (Atom.Bval_inj2 _ _ (v_vald1) (store v_vale1 v_vale2 v_vale3) Htid1'').
+          
+          rewrite Htie1 in Htic1.
+
+
+          rewrite (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) (v_vale1) (v_valc1) Htic1).
+
+          simpl in isif. rewrite !Typ.cast_refl in isif.
+          apply Typ.i_eqb_spec_false in isif.
+
+          rewrite !Atom.t_interp_wf in Htic2''; trivial.
+
+          destruct Heq11d as [((Heq11d1,Heq11d2),Heq11d3) | ((Heq11d1,Heq11d2),Heq11d3) ];
+            subst; intros;
+
+              rewrite Htid2 in Htic2;
+              rewrite <- (Atom.Bval_inj2 _ _  (v_vald2) (v_valc2) Htic2) in *. 
+          
+          + rewrite Htie2 in Htia1.
+            rewrite Htia2 in Htic2''.
+            rewrite <- (Atom.Bval_inj2 _ _ _ _ Htia1) in *.
+            rewrite (Atom.Bval_inj2 _ _ _ _ Htic2'') in *.
+            symmetry; now apply read_over_other_write.
+
+          + rewrite Htie2 in Htia2.
+            rewrite Htia1 in Htic2''.
+            rewrite <- (Atom.Bval_inj2 _ _ _ _ Htia2) in *.
+            rewrite (Atom.Bval_inj2 _ _ _ _ Htic2'') in *.
+            symmetry; apply read_over_other_write; now auto.
+
+
+        - unfold store_of_me.
+          case_eq (t_atom .[ c1]); try discriminate.
+          intros [ t5 t6 ] e1 e2 e3 Heq10 [[ti3 te3] i1].
+          case_eq (e1 == d1); try discriminate. intros Heq11d.
+          intro HT.
+          injection HT. intros E2 T6 T5 [ ]. subst i1 te3 ti3. clear HT.
+
+          case_eq (
+              Typ.eqb t t5 && Typ.eqb v_typeb1' t6 &&
+                      ((e2 == a1) && (c2 == a2) && (d2 == a2) || (e2 == a2) && (c2 == a1) && (d2 == a1)));
+            simpl; intros Heq11; try (now apply C.interp_true).
+
+          unfold C.valid. simpl. rewrite orb_false_r.
+
+          case_eq (Lit.interp rho i). intros isit.
+          easy. intros isif. rewrite orb_false_l.
+          specialize (rho_interp ( Lit.blit i)).
+          rewrite Heq3 in rho_interp.
+          simpl in rho_interp.
+          unfold Lit.interp in isif.
+          rewrite Heq in isif. unfold Var.interp in isif.
+          rewrite rho_interp in isif.
+          unfold Atom.interp_form_hatom, interp_hatom in isif.
+          rewrite Atom.t_interp_wf in isif; trivial.
+          rewrite Heq5 in isif.
+          simpl in isif.
+          unfold interp_bool in isif.
+
+          unfold Lit.interp. rewrite Heq2.
+          unfold Var.interp.
+          rewrite !wf_interp_form; trivial. rewrite Heq4. simpl.
+
+          rewrite !andb_true_iff in Heq11.
+          destruct Heq11 as ((Heq11a, Heq11b), Heq11c).
+          rewrite !orb_true_iff in Heq11c.
+
+          apply Typ.eqb_spec in Heq11a.
+          apply Typ.eqb_spec in Heq11b.
+          apply Int63Properties.eqb_spec in Heq11d.
+          rewrite !andb_true_iff in Heq11c.
+          rewrite !Int63Properties.eqb_spec in Heq11c.
+
+
+          rewrite !Atom.t_interp_wf in isif; trivial.
+          rewrite Htia1, Htia2 in isif. simpl in isif.
+          unfold Bval in isif.
+          rewrite !Typ.cast_refl in isif.
+          
+
+          assert (H25: c1 < PArray.length t_atom).
+          apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq10. discriminate.
+          apply H2 in H25.
+          rewrite Heq10 in H25.
+          simpl in H25.
+          rewrite !andb_true_iff in H25.
+          destruct H25 as (((H25, H29), H28), H27).
+          unfold get_type', v_type in H25, H27, H28, H29.
+
+          case_eq (t_interp .[ c1]).
+          intros v_typec1' v_valc1' Htic1'. rewrite Htic1' in H25.
+          case_eq v_typec1'; intros; rewrite H10 in H25; try now contradict H25.
+          rewrite andb_true_iff in H25; destruct H25 as (H25a, H25b).
+
+          case_eq (t_interp .[ e1]).
+          intros v_typee1 v_vale1 Htie1. rewrite Htie1 in H29.
+          case_eq (t_interp .[ e2]).
+          intros v_typee2 v_vale2 Htie2. rewrite Htie2 in H28.
+          case_eq (t_interp .[ e3]).
+          intros v_typee3 v_vale3 Htie3. rewrite Htie3 in H27.
+          pose proof Htic1' as Htic1''.
+          rewrite Atom.t_interp_wf in Htic1', Htie1, Htie2, Htie3; trivial.
+          rewrite Heq10 in Htic1'. simpl in Htic1'.
+          rewrite !Atom.t_interp_wf in Htic1'; trivial.
+          rewrite Htie1, Htie2, Htie3 in Htic1'. simpl in Htic1'.
+
+          apply Typ.eqb_spec in H25a. apply Typ.eqb_spec in H25b.
+          apply Typ.eqb_spec in H27.  apply Typ.eqb_spec in H28.
+          apply Typ.eqb_spec in H29.
+
+          generalize dependent v_vale1. generalize dependent v_vale2.
+          generalize dependent v_vale3. generalize dependent v_valc1'.
+          rewrite H27, H28, H29.
+          rewrite !Typ.cast_refl. intros. simpl in Htic1'.
+          unfold Bval in Htic1'.
+
+
+          generalize dependent v_vale1. generalize dependent v_vale2.
+          generalize dependent v_vale3. generalize dependent v_valc1'.
+
+          rewrite H25a, H25b, H10. intros.
+          specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2)
+                                     (store v_vale1 v_vale2 v_vale3) (v_valc1')).
+          intro H25. specialize (H25 Htic1').
+          
+          unfold Atom.interp_form_hatom, interp_hatom.
+          rewrite !Atom.t_interp_wf; trivial.
+          rewrite Heq6. simpl.
+          rewrite !Atom.t_interp_wf; trivial.
+          rewrite Heq7, Heq8. simpl.
+          rewrite !Atom.t_interp_wf; trivial.
+
+          rewrite Htid1, Htic2, Htic1, Htid2.
+          subst. intros. simpl.
+          rewrite !Typ.cast_refl.
+          unfold apply_binop.
+          unfold Bval.
+          rewrite !Atom.t_interp_wf in Htib1''; trivial.
+          rewrite Htib1 in Htib1''.
+          inversion Htib1''.
+          rewrite !Atom.t_interp_wf in Htib2''; trivial.
+          rewrite Htib2 in Htib2''.
+          inversion Htib2''.
+
+          rewrite !Typ.cast_refl.
+
+          unfold interp_bool. rewrite Typ.cast_refl.
+          apply Typ.i_eqb_spec.
+
+          rewrite !Atom.t_interp_wf in Htic1''; trivial.
+          rewrite Htic1 in Htic1''.
+          inversion Htic1''.
+
+          subst.
+          rewrite (Atom.Bval_inj2 _ _ (v_valc1) (store v_vale1 v_vale2 v_vale3) Htic1'').
+          
+          rewrite Htie1 in Htid1.
+
+
+          rewrite (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) (v_vale1) (v_vald1) Htid1).
+
+          apply Typ.i_eqb_spec_false in isif.
+
+          rewrite !Atom.t_interp_wf in Htic2''; trivial.
+
+          destruct Heq11c as [((Heq11c1,Heq11c2),Heq11c3) | ((Heq11c1,Heq11c2),Heq11c3) ];
+            subst; intros;
+
+              rewrite Htid2 in Htic2;
+              rewrite <- (Atom.Bval_inj2 _ _  (v_vald2) (v_valc2) Htic2) in *. 
+          
+          + rewrite Htie2 in Htia1.
+            rewrite Htia2 in Htic2''.
+            rewrite <- (Atom.Bval_inj2 _ _ _ _ Htia1) in *.
+            rewrite (Atom.Bval_inj2 _ _ _ _ Htic2'') in *.
+            now apply read_over_other_write.
+
+          + rewrite Htie2 in Htia2.
+            rewrite Htia1 in Htic2''.
+            rewrite <- (Atom.Bval_inj2 _ _ _ _ Htia2) in *.
+            rewrite (Atom.Bval_inj2 _ _ _ _ Htic2'') in *.
+            apply read_over_other_write; now auto.
+    Qed.
+
+  Axiom afold_left_or : forall a,
+    afold_left bool int false orb (Lit.interp rho) a =
+    C.interp rho (to_list a).
+
+  Require Import Psatz.
+
+  Lemma valid_check_ext lres : C.valid rho (check_ext lres).
+    unfold check_ext, eq_sel_sym.
+    case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true.
+    case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
+    intros a Heq2.
+    case_eq (length a == 2); [ intros Heq3 | intros Heq3; now apply C.interp_true].
+    case_eq (Lit.is_pos (a .[ 0]) && negb (Lit.is_pos (a .[ 1])));
+      [ intros Heq4 | intros Heq4; now apply C.interp_true].
+    case_eq (t_form .[ Lit.blit (a .[0])]); try (intros; now apply C.interp_true).
+    intros b Heq5.
+    case_eq (t_form .[ Lit.blit (a .[1])]); try (intros; now apply C.interp_true).
+    intros c Heq6.
+    case_eq (t_atom .[ b]); try (intros; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] b1 b2 Heq7; try (intros; now apply C.interp_true).
+    case_eq t; try (intros; now apply C.interp_true). intros t0 t1 Heq8.
+    case_eq (t_atom .[ c]); try (intros; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] c1 c2 Heq9; try (intros; now apply C.interp_true).
+    case_eq (Typ.eqb t1 t2); [ intros Heq10 | intros Heq10; now apply C.interp_true].
+    case_eq (t_atom .[ c1]); try (intros; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] d1 d2 Heq11; try (intros; now apply C.interp_true).
+    case_eq (t_atom .[ c2]); try (intros; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] e1 e2 Heq12; try (intros; now apply C.interp_true).
+    case_eq (t_atom .[ d2]);
+      try (intros; rewrite !andb_false_r; simpl; now apply C.interp_true).
+    intros [ | | | | | | | |N|N|N|N|N|N|N|N|N| | | | ] f1 f2 Heq14;
+      try (intros; rewrite !andb_false_r; simpl; now apply C.interp_true).
+    case_eq (Typ.eqb t0 t3 && Typ.eqb t0 t5 && Typ.eqb t1 t4 && Typ.eqb t1 t6);
+      [ intros Heq13'| intro; now apply C.interp_true].
+    simpl.
+    case_eq (Typ.eqb t0 t7 && Typ.eqb t1 t8);
+      [ intros Heq14'| intro; rewrite !andb_false_r; simpl; now apply C.interp_true].
+    simpl.
+    case_eq ((b1 == d1) && (b2 == e1) && (d2 == e2) && ((f1 == b1) && (f2 == b2))
+             || (b2 == d1) && (b1 == e1) && (d2 == e2) && ((f1 == b2) && (f2 == b1)));
+        [ intros Heq1314 | intro; now apply C.interp_true].
+
+    unfold C.valid. simpl. rewrite orb_false_r.
+
+    rewrite orb_true_iff in Heq1314.
+    rewrite !andb_true_iff in Heq13'.
+    rewrite !andb_true_iff in Heq14'.
+    rewrite !andb_true_iff in Heq1314.
+    destruct Heq13' as (((Heq13, Heq13f), Heq13a), Heq13d).
+    destruct Heq14' as (Heq15, Heq15a).
+
+    apply Typ.eqb_spec in Heq13.
+    apply Typ.eqb_spec in Heq13f.
+    apply Typ.eqb_spec in Heq13a.
+    apply Typ.eqb_spec in Heq13d.
+    apply Typ.eqb_spec in Heq15.
+    apply Typ.eqb_spec in Heq15a.
+    subst t3 t5 t4 t6 t7 t8.
+    rewrite !Int63Properties.eqb_spec in Heq1314.
+
+    unfold Lit.interp. rewrite Heq.
+    unfold Var.interp.
+    rewrite !wf_interp_form; trivial. rewrite Heq2. simpl.
+    rewrite afold_left_or.
+    unfold to_list.
+    rewrite Int63Properties.eqb_spec in Heq3.
+    rewrite Heq3.
+
+    (* for native-coq compatibility *)
+    assert (0 == 2 = false) as NCC.
+    { auto. } rewrite NCC.
+    (* simpl. *)
+    rewrite foldi_down_gt; auto.
+
+    (* simpl. *)
+    assert (2 - 1 = 1). { auto. }
+                        rewrite H.
+    rewrite foldi_down_eq; auto. 
+    simpl. rewrite orb_false_r.
+    assert (1 - 1 = 0) as Has2. { auto. }
+                                rewrite Has2.
+
+    case_eq (Lit.interp rho (a .[ 0])). intro Hisa0.
+    rewrite orb_true_l. easy. intro Hisa. rewrite orb_false_l.
+
+    pose proof (rho_interp (Lit.blit (a .[ 0]))).
+    pose proof (rho_interp (Lit.blit (a .[ 1]))).
+
+    rewrite Heq5 in H0. rewrite Heq6 in H1.
+    simpl in H0, H1.
+    unfold Lit.interp.
+    rewrite andb_true_iff in Heq4.
+    destruct Heq4 as (Heq4, Heq4a).
+    apply negb_true_iff in Heq4a.
+
+    unfold Lit.interp in Hisa.
+    rewrite Heq4 in Hisa. unfold Var.interp in Hisa.
+    rewrite Hisa in H0. symmetry in H0.
+    rewrite Heq4a.
+    unfold Var.interp.
+    rewrite H1.
+
+    generalize wt_t_atom. unfold Atom.wt. unfold is_true.
+    rewrite PArray.forallbi_spec;intros.
+
+    (* b *)
+    pose proof (H2 b). assert (b < PArray.length t_atom).
+    apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq7. easy.
+    specialize (H3 H4). simpl in H3.
+    rewrite Heq7 in H3. simpl in H3.
+    rewrite !andb_true_iff in H3. destruct H3. destruct H3.
+    unfold get_type' in H3, H5, H6. unfold v_type in H3, H5, H6.
+
+    case_eq (t_interp .[ b]).
+    intros v_typeb v_valb Htib. rewrite Htib in H3.
+    pose proof Htib as Htib''.
+    case_eq v_typeb; intros; rewrite H7 in H3; try now contradict H3.
+
+    case_eq (t_interp .[ b1]).
+    intros v_typeb1 v_valb1 Htib1. rewrite Htib1 in H6.
+    pose proof Htib1 as Htib1''.
+    case_eq (t_interp .[ b2]).
+    intros v_typeb2 v_valb2 Htib2. rewrite Htib2 in H5.
+    pose proof Htib2 as Htib2''.
+    rewrite Atom.t_interp_wf in Htib; trivial.
+    rewrite Atom.t_interp_wf in Htib1; trivial.
+    rewrite Atom.t_interp_wf in Htib2; trivial.
+    rewrite Heq7 in Htib. simpl in Htib.
+    rewrite !Atom.t_interp_wf in Htib; trivial.
+    rewrite Htib1, Htib2 in Htib.
+    unfold apply_binop in Htib.
+    apply Typ.eqb_spec in H5.
+    apply Typ.eqb_spec in H6.
+
+    generalize dependent v_valb1. generalize dependent v_valb2.
+    generalize dependent v_valb.
+    rewrite H5, H6, H7. rewrite !Typ.cast_refl. intros.
+
+    specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t v_valb1 v_valb2) (v_valb)).
+    intros. specialize (H8 Htib).
+
+    (* c *)
+    pose proof (H2 c). assert (c < PArray.length t_atom).
+    apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy.
+    specialize (H9 H10). simpl in H9.
+    rewrite Heq9 in H9. simpl in H9.
+    rewrite !andb_true_iff in H9. destruct H9. destruct H9.
+    unfold get_type' in H9, H11, H12. unfold v_type in H9, H11, H12.
+
+    case_eq (t_interp .[ c]).
+    intros v_typec v_valc Htic. rewrite Htic in H9.
+    pose proof Htic as Htic''.
+    case_eq v_typec; intros; rewrite H13 in H9; try now contradict H9.
+
+    case_eq (t_interp .[ c1]).
+    intros v_typec1 v_valc1 Htic1. rewrite Htic1 in H12.
+    case_eq (t_interp .[ c2]).
+    intros v_typec2 v_valc2 Htic2. rewrite Htic2 in H11.
+    rewrite Atom.t_interp_wf in Htic; trivial.
+    rewrite Atom.t_interp_wf in Htic1; trivial.
+    rewrite Atom.t_interp_wf in Htic2; trivial.
+    rewrite Heq9 in Htic. simpl in Htic.
+    rewrite !Atom.t_interp_wf in Htic; trivial.
+    rewrite Htic1, Htic2 in Htic. simpl in Htic.
+
+    apply Typ.eqb_spec in H11. apply Typ.eqb_spec in H12.
+
+    generalize dependent v_valc1. generalize dependent v_valc2.
+    generalize dependent v_valc.
+    rewrite H11, H12, H13.
+    rewrite !Typ.cast_refl. intros. simpl in Htic.
+    unfold Bval in Htic.
+
+    specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t2 v_valc1 v_valc2) (v_valc)).
+    intros. specialize (H14 Htic).
+
+    (* c1 *)
+    pose proof (H2 c1). assert (c1 < PArray.length t_atom).
+    apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq11. easy.
+    specialize (H15 H16). simpl in H15.
+    rewrite Heq11 in H15. simpl in H15.
+    rewrite !andb_true_iff in H15. destruct H15. destruct H15.
+    unfold get_type' in H15, H17, H18. unfold v_type in H15, H17, H18.
+
+    case_eq (t_interp .[ c1]).
+    intros v_typec1' v_valc1' Htic1'. rewrite Htic1' in H15.
+    pose proof Htic1' as Htic1'''.
+
+    case_eq (t_interp .[ d1]).
+    intros v_typed1 v_vald1 Htid1. rewrite Htid1 in H18.
+    case_eq (t_interp .[ d2]).
+    intros v_typed2 v_vald2 Htid2. rewrite Htid2 in H17.
+    rewrite Atom.t_interp_wf in Htic1'; trivial.
+    rewrite Atom.t_interp_wf in Htid1; trivial.
+    rewrite Atom.t_interp_wf in Htid2; trivial.
+    rewrite Heq11 in Htic1'. simpl in Htic1'.
+    rewrite !Atom.t_interp_wf in Htic1'; trivial.
+    rewrite Htid1, Htid2 in Htic1'. simpl in Htic1'.
+
+    apply Typ.eqb_spec in H15. apply Typ.eqb_spec in H17.
+    apply Typ.eqb_spec in H18.
+
+    generalize dependent v_vald1. generalize dependent v_vald2.
+    generalize dependent v_valc1'.
+
+    rewrite H15, H17, H18.
+    unfold Bval. rewrite <- H15.
+    rewrite !Typ.cast_refl. intros.
+
+    specialize (Atom.Bval_inj2 t_i t1 (select v_vald1 v_vald2) (v_valc1')).
+    intros. specialize (H19 Htic1').
+
+    (* c2 *)
+    pose proof (H2 c2). assert (c2 < PArray.length t_atom).
+    apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq12. easy.
+    specialize (H20 H21). simpl in H20.
+    rewrite Heq12 in H20. simpl in H20.
+    rewrite !andb_true_iff in H20. destruct H20. destruct H20.
+    unfold get_type' in H20, H22, H23. unfold v_type in H20, H22, H23.
+
+    case_eq (t_interp .[ c2]).
+    intros v_typec2' v_valc2' Htic2'. rewrite Htic2' in H20.
+    pose proof Htic2' as Htic2'''.
+
+    case_eq (t_interp .[ e1]).
+    intros v_typee1 v_vale1 Htie1. rewrite Htie1 in H23.
+    case_eq (t_interp .[ e2]).
+    intros v_typee2 v_vale2 Htie2. rewrite Htie2 in H22.
+    pose proof Htie2 as Htie2''.
+    rewrite Atom.t_interp_wf in Htic2'; trivial.
+    rewrite Atom.t_interp_wf in Htie1; trivial.
+    rewrite Atom.t_interp_wf in Htie2; trivial.
+    rewrite Heq12 in Htic2'. simpl in Htic2'.
+    rewrite !Atom.t_interp_wf in Htic2'; trivial.
+    rewrite Htie1, Htie2 in Htic2'. simpl in Htic2'.
+
+    apply Typ.eqb_spec in H20. apply Typ.eqb_spec in H22.
+    apply Typ.eqb_spec in H23.
+
+    generalize dependent v_valc1'. generalize dependent v_valc2'.
+    generalize dependent v_vale1. generalize dependent v_vale2.
+
+    rewrite H22. rewrite H20 in *. rewrite H23.
+    unfold Bval. rewrite <- H20.
+    rewrite !Typ.cast_refl. intros.
+
+    specialize (Atom.Bval_inj2 t_i t1 (select v_vale1 v_vale2) (v_valc2')).
+    intros. specialize (H24 Htic2').
+
+    (* d2 *)
+    pose proof (H2 d2). assert (d2 < PArray.length t_atom).
+    apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq14. easy.
+    specialize (H25 H26). simpl in H25.
+    rewrite Heq14 in H25. simpl in H25.
+    rewrite !andb_true_iff in H25. destruct H25. destruct H25.
+    unfold get_type' in H25, H27, H28. unfold v_type in H25, H27, H28.
+
+    case_eq (t_interp .[ d2]).
+    intros v_typed2' v_vald2' Htid2'. rewrite Htid2' in H25.
+    pose proof Htid2' as Htid2'''.
+
+    case_eq (t_interp .[ f1]).
+    intros v_typef1 v_valf1 Htif1. rewrite Htif1 in H28.
+    case_eq (t_interp .[ f2]).
+    intros v_typef2 v_valf2 Htif2. rewrite Htif2 in H27.
+    rewrite Atom.t_interp_wf in Htid2'; trivial.
+    rewrite Atom.t_interp_wf in Htif1; trivial.
+    rewrite Atom.t_interp_wf in Htif2; trivial.
+    rewrite Heq14 in Htid2'. simpl in Htid2'.
+    rewrite !Atom.t_interp_wf in Htid2'; trivial.
+    rewrite Htif1, Htif2 in Htid2'. simpl in Htid2'.
+
+    apply Typ.eqb_spec in H25. apply Typ.eqb_spec in H27.
+    apply Typ.eqb_spec in H28.
+
+    generalize dependent v_valf1. generalize dependent v_valf2.
+    generalize dependent v_vald2'.
+
+    rewrite H25, H27, H28.
+    unfold Bval. rewrite <- H25.
+    rewrite !Typ.cast_refl. intros.
+
+    specialize (Atom.Bval_inj2 t_i t0 (diff v_valf1 v_valf2) (v_vald2')).
+    intros. specialize (H29 Htid2').
+
+    (* semantics *)
+
+    unfold Atom.interp_form_hatom, interp_hatom.
+    rewrite !Atom.t_interp_wf; trivial.
+    rewrite Heq9. simpl.
+    rewrite !Atom.t_interp_wf; trivial.
+    rewrite  Heq11, Heq12. simpl.
+
+    unfold apply_binop.
+    rewrite !Atom.t_interp_wf; trivial.
+    rewrite Htid1, Heq14, Htie1, Htie2.
+    rewrite !Typ.cast_refl.
+    simpl. (* (* native-coq compatibility *) unfold interp_atom. *)
+    rewrite !Atom.t_interp_wf; trivial.
+    rewrite Htif1, Htif2. simpl.
+    rewrite !Typ.cast_refl. simpl.
+
+    rewrite !Atom.t_interp_wf in Htid2'''; trivial.
+    rewrite Htid2 in Htid2'''.
+    inversion Htid2'''.
+
+    rewrite !Atom.t_interp_wf in Htic1'''; trivial.
+    rewrite Htic1 in Htic1'''.
+    inversion Htic1'''.
+
+    rewrite !Atom.t_interp_wf in Htic2'''; trivial.
+    rewrite Htic2 in Htic2'''.
+    inversion Htic2'''.
+
+    generalize dependent v_valc1. generalize dependent v_valc2.
+    generalize dependent v_valc1'. generalize dependent v_valc2'.
+    generalize dependent v_vald1. generalize dependent v_vald2.
+
+    subst.
+    rewrite !Typ.cast_refl. simpl.
+    rewrite !Typ.cast_refl. intros. simpl.
+
+    apply negb_true_iff.
+    apply Typ.i_eqb_spec_false.
+    subst.
+    specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (diff v_valf1 v_valf2)).
+    intros. specialize (H5 Htid2''').
+    rewrite <- H5.
+    specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)).
+    intros.
+
+    unfold Atom.interp_form_hatom, interp_hatom in H0.
+    rewrite !Atom.t_interp_wf in H0; trivial.
+    rewrite Heq7 in H0. simpl in H0.
+    rewrite !Atom.t_interp_wf in H0; trivial.
+    rewrite Htib1, Htib2 in H0. simpl in H0.
+    rewrite !Typ.cast_refl in H0. simpl in H0.
+    apply Typ.i_eqb_spec_false in H0.
+
+
+    destruct Heq1314 as [Heq1314 | Heq1314];
+      destruct Heq1314 as (((Heq13a, Heq13b), Heq13c), (Heq13d, Heq13e));
+      subst.
+
+    - rewrite Htie2 in Htid2.
+      rewrite Htid1 in Htib1.
+      rewrite Htie1 in Htib2.
+      rewrite Htid1 in Htif1.
+      rewrite Htie1 in Htif2.
+
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htib1) in *.
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htib2) in *.
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htif1) in *.
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htif2) in *.
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htid2) in *.
+
+      now apply select_at_diff.
+
+    - rewrite Htie2 in Htid2.
+      rewrite Htid1 in Htib2.
+      rewrite Htie1 in Htib1.
+      rewrite Htid1 in Htif1.
+      rewrite Htie1 in Htif2.
+
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htib1) in *.
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htib2) in *.
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htif1) in *.
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htif2) in *.
+      rewrite (Atom.Bval_inj2 t_i _ _ _ Htid2) in *.
+
+      apply select_at_diff.
+      red in H0. red. intro. apply H0. auto.
+  Qed.
+  
+  End Correct.
+
+End certif.