port to 8.6 and new Travis/OPAm approach

Author: palmskog

.travis-ci.sh

@@ -7,38 +7,21 @@ opam repo add coq-released https://coq.inria.fr/opam/released
 opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
 
 opam pin add coq $COQ_VERSION --yes --verbose
-opam pin add coq-mathcomp-ssreflect $SSREFLECT_VERSION --yes --verbose
-opam pin add coq-aac-tactics $AAC_TACTICS_VERSION --yes --verbose
-
-opam install coq-mathcomp-fingroup coq-mathcomp-algebra StructTact InfSeqExt verdi verdi-cheerios --yes --verbose
 
 case $MODE in
-  analytics)
-    ./script/analytics.sh &
+  proofalytics)
+    opam pin add verdi-aggregation-proofalytics . --yes --verbose &
     # Output to the screen every 9 minutes to prevent a travis timeout
     export PID=$!
     while [[ `ps -p $PID | tail -n +2` ]]; do
 	echo 'proofalyzing...'
 	sleep 540
     done
     ;;
-  tree-test)
-    opam install verdi-runtime ounit.2.0.0 uuidm.0.9.6 --yes --verbose
-    ./build.sh tree-test
-    ;;
-  tree-dynamic-test)
-    opam install verdi-runtime ounit.2.0.0 uuidm.0.9.6 --yes --verbose
-    ./build.sh tree-dynamic-test
-    ;;
-  aggregation-test)
-    opam install verdi-runtime ounit.2.0.0 uuidm.0.9.6 --yes --verbose
-    ./build.sh aggregation-test
-    ;;
-  aggregation-dynamic-test)
-    opam install verdi-runtime ounit.2.0.0 uuidm.0.9.6 portaudio.0.2.1 --yes --verbose
-    ./build.sh aggregation-dynamic-test
+  aggregation-dynamic)
+    opam pin add aggregation-dynamic . --yes --verbose
     ;;
   *)
-    ./build.sh
+    opam pin add verdi-aggregation . --yes --verbose
     ;;
 esac

.travis.yml

@@ -10,14 +10,11 @@ addons:
       - portaudio19-dev
 env:
   global:
-    - COQ_VERSION=8.5.3
-    - SSREFLECT_VERSION=1.6
-    - AAC_TACTICS_VERSION=8.5.1
+    - COQ_VERSION=8.6
   matrix:
     - MODE=build
-    - MODE=aggregation-test
-    - MODE=aggregation-dynamic-test
-    - MODE=analytics
+    - MODE=aggregation-dynamic OPAMBUILDTEST=1
+    - MODE=proofalytics
 before_install:
   - openssl aes-256-cbc -K $encrypted_80476f3400be_key -iv $encrypted_80476f3400be_iv -in .travis/travis_rsa.enc -out .travis/travis_rsa -d
   - cp .travis/travis_rsa ~/.ssh

Makefile

@@ -1,8 +1,8 @@
 PYTHON=python2.7
-COQVERSION := $(shell coqc --version|grep "version 8.5")
+COQVERSION := $(shell coqc --version|egrep "version (8\\.6|trunk)")
 
 ifeq "$(COQVERSION)" ""
-$(error "Verdi Aggregation is only compatible with Coq version 8.5")
+$(error "Verdi Aggregation is only compatible with Coq version 8.6")
 endif
 
 COQPROJECT_EXISTS=$(wildcard _CoqProject)

aggregation-dynamic.install

@@ -0,0 +1 @@
+bin: ["extraction/aggregation-dynamic/_build/ocaml/TreeAggregationMain.native" {"aggregation-dynamic"}]

aggregation-dynamic.opam

@@ -0,0 +1,38 @@
+opam-version: "1.2"
+version: "dev"
+maintainer: "[email protected]"
+
+homepage: "https://github.com/DistributedComponents/verdi-aggregation"
+dev-repo: "https://github.com/DistributedComponents/verdi-aggregation.git"
+bug-reports: "https://github.com/DistributedComponents/verdi-aggregation/issues"
+license: "Proprietary"
+
+build: [
+  [ "./configure" ]
+  [ make "-j%{jobs}%" "aggregation-dynamic" ]
+]
+build-test: [make "aggregation-dynamic-test"]
+available: [ ocaml-version >= "4.02.3" ]
+depends: [
+  "coq" {>= "8.6" & < "8.7~"}
+  "coq-mathcomp-ssreflect" {>= "1.6" & < "1.7~"}
+  "coq-mathcomp-algebra" {>= "1.6" & < "1.7~"}
+  "coq-mathcomp-fingroup" {>= "1.6" & < "1.7~"}
+  "coq-aac-tactics" {>= "8.6.1"}
+  "verdi" {= "dev"}
+  "StructTact" {= "dev"}
+  "InfSeqExt" {= "dev"}
+  "cheerios" {= "dev"}
+  "verdi-cheerios" {= "dev"}
+  "ocamlbuild" {build}
+  "ocamlfind" {build}
+  "verdi-runtime" {= "dev"}
+  "uuidm" {>= "0.9.6"}
+  "portaudio" {>= "0.2.1"}
+  "ounit" {test & >= "2.0.0"}
+]
+
+authors: [
+  "Karl Palmskog <>"
+  "Ryan Doenges <>"
+]

systems/AggregationDynamicCorrect.v

@@ -17,6 +17,7 @@ Require Import Orders.
 Require Import MSetFacts.
 Require Import MSetProperties.
 Require Import Sorting.Permutation.
+Require FMapFacts.
 
 Require Import mathcomp.ssreflect.ssreflect.
 Require Import mathcomp.ssreflect.ssrbool.
@@ -60,7 +61,7 @@ Module NSetFacts := Facts NSet.
 Module NSetProps := Properties NSet.
 Module NSetOrdProps := OrdProperties NSet.
 
-Require Import FMapFacts.
+Import FMapFacts.
 Module NMapFacts := Facts NMap.
 
 Instance Aggregation_FailureRecorder_base_params_pt_map : BaseParamsPartialMap Aggregation_BaseParams FR.FailureRecorder_BaseParams :=
@@ -960,7 +961,7 @@ end; simpl in *.
   by auto.
 - find_apply_lem_hyp net_handlers_NetHandler.
   net_handler_cases => //=; unfold update2, update in *; simpl in *; repeat break_if; break_and; subst_max; try find_injection; try by eauto.
-  * have H_in: In (Aggregate x) (odnwPackets net0 n' n) by repeat find_rewrite; left.
+  * have H_in: In (Aggregate x) (odnwPackets net0 n' to) by repeat find_rewrite; left.
     have IH := IHrefl_trans_1n_trace1 _ H6 H7 _ H8 _ H_in _ H4.
     find_rewrite.
     break_or_hyp; last by right; find_reverse_rewrite.
@@ -1163,7 +1164,7 @@ have H_bef := Aggregation_in_after_all_aggregate_new H_st _ H_n H_f _ H_dec m'.
 destruct (odnwPackets net n' n) => //.
 simpl in *.
 find_injection.
-move => H_in'.
+move => H_in' {H_in}.
 break_or_hyp => //.
 break_or_hyp => //.
 by break_and.
@@ -1638,7 +1639,7 @@ end; simpl in *.
     by break_and.
   * have H_neq: from <> to.
       move => H_eq.
-      find_rewrite.
+      repeat find_rewrite.
       by rewrite (Aggregation_self_channel_empty s1) in H3.
     case (in_dec name_eq_dec from net.(odnwNodes)) => H_dec; last by rewrite (@ordered_dynamic_no_outgoing_uninitialized _ _ _ _ Aggregation_FailMsgParams _ _ _ s1) in H3.
     case (in_dec name_eq_dec from failed0) => H_dec'; last first.
@@ -1662,7 +1663,7 @@ end; simpl in *.
     by congruence.
   * have H_neq: from <> to.
       move => H_eq.
-      find_rewrite.
+      repeat find_rewrite.
       by rewrite (Aggregation_self_channel_empty s1) in H3.
     case (in_dec name_eq_dec from net.(odnwNodes)) => H_dec; last by rewrite (@ordered_dynamic_no_outgoing_uninitialized _ _ _ _ Aggregation_FailMsgParams _ _ _ s1) in H3.
     unfold update2, update in *.
@@ -2368,10 +2369,10 @@ end; simpl.
   net_handler_cases.
   * destruct_update; repeat find_injection.
     + rewrite /update2 /=.
-      break_if; first by break_and; subst; find_rewrite_lem (Aggregation_self_channel_empty s1).
+      break_if; first by break_and; subst; repeat find_rewrite_lem (Aggregation_self_channel_empty s1).
       break_or_hyp => //.
       case (In_dec name_eq_dec from net.(odnwNodes)) => H_from_in; last by find_rewrite_lem (@ordered_dynamic_no_outgoing_uninitialized _ _ _ _ Aggregation_FailMsgParams _ _ _ s1 _ H_from_in).
-      destruct d1.
+      destruct d0.
       simpl in *.
       rewrite (Aggregation_self_channel_empty s1).
       repeat find_rewrite.
@@ -2423,14 +2424,14 @@ end; simpl.
     by find_rewrite.
   * destruct_update; repeat find_injection.
     + rewrite /update2 /=.
-      break_if; first by break_and; subst; find_rewrite_lem (Aggregation_self_channel_empty s1).
+      break_if; first by break_and; subst; repeat find_rewrite_lem (Aggregation_self_channel_empty s1).
       break_or_hyp => //.
       case (In_dec name_eq_dec from net.(odnwNodes)) => H_from_in; last by find_rewrite_lem (@ordered_dynamic_no_outgoing_uninitialized _ _ _ _ Aggregation_FailMsgParams _ _ _ s1 _ H_from_in).
       case (In_dec name_eq_dec from failed0) => H_from_f; last first.
         have H_f := Aggregation_not_failed_no_fail s1 _ H_from_in H_from_f n.
         rewrite H3 in H_f.
         by case: H_f; left.
-      destruct d1.
+      destruct d0.
       simpl in *.
       rewrite (Aggregation_self_channel_empty s1).
       repeat find_rewrite.
@@ -2488,10 +2489,10 @@ end; simpl.
     by find_rewrite.
   * destruct_update; repeat find_injection.
     + rewrite /update2 /=.
-      break_if; first by break_and; subst; find_rewrite_lem (Aggregation_self_channel_empty s1).
+      break_if; first by break_and; subst; repeat find_rewrite_lem (Aggregation_self_channel_empty s1).
       break_or_hyp => //.
       case (In_dec name_eq_dec from net.(odnwNodes)) => H_from_in; last by find_rewrite_lem (@ordered_dynamic_no_outgoing_uninitialized _ _ _ _ Aggregation_FailMsgParams _ _ _ s1 _ H_from_in).     
-      destruct d1.
+      destruct d0.
       simpl in *.
       rewrite (Aggregation_self_channel_empty s1).
       repeat find_rewrite.
@@ -2543,7 +2544,7 @@ end; simpl.
   io_handler_cases.
   * destruct_update; repeat find_injection.
     + rewrite /= (Aggregation_self_channel_empty s1).
-      destruct d1.
+      destruct d0.
       simpl in *.
       repeat find_rewrite.      
       by apply: (recv_local_self _ s1); eauto.
@@ -2567,7 +2568,7 @@ end; simpl.
       have H_x_in: In x net.(odnwNodes).
         have H_or := Aggregation_in_adj_or_incoming_fail s1 _ H_in_n H_in_f H2 H3.
         by break_or_hyp; break_and.
-      destruct d1.
+      destruct d0.
       simpl in *.
       repeat find_rewrite.
       apply: (send_aggregate_self s1) => //.
@@ -2896,7 +2897,7 @@ apply: (P_dual_inv H_st); rewrite /P_curr //= {P_curr tr H_st failed H_f H_f' H_
 - move => net failed tr from ms m0 H_st H_in_n H_in_f H_eq H_in_from H_in_from' H_neq H_adj H_eq'. 
   move => d H_eq_d H_find IH H_ins H_ins' m1 H_find_m1 m2 H_find_m2.
   subst.
-  find_apply_lem_hyp NSetFacts.remove_3.
+  repeat find_apply_lem_hyp NSetFacts.remove_3.
   contradict H_ins.
   by eapply Aggregation_node_not_adjacent_self; eauto.
 - move => net failed tr from ms m0 H_st H_in_n H_in_f H_in_n' H_in_f' H_neq H_from_neq H_from_neq' H_in_from H_in_from' H_adj H_eq.
@@ -2912,7 +2913,7 @@ apply: (P_dual_inv H_st); rewrite /P_curr //= {P_curr tr H_st failed H_f H_f' H_
 - move => net faild tr from ms H_st H_in_n H_in_f H_eq H_in_from H_neq_from H_adj H_eq'.
   move => d H_eq_d IH H_ins H_ins' m0 H_find_m0 m1 H_find_m1.
   subst.
-  find_apply_lem_hyp NSetFacts.add_3 => //.
+  repeat find_apply_lem_hyp NSetFacts.add_3 => //.
   contradict H_ins.
   by eapply Aggregation_node_not_adjacent_self; eauto.
 - move => net failed tr ms H_st H_in_n H_in_f H_in_n' H_in_f' H_neq H_adj H_eq.

systems/AggregationStaticCorrect.v

@@ -18,6 +18,7 @@ Require Import Orders.
 Require Import MSetFacts.
 Require Import MSetProperties.
 Require Import Sorting.Permutation.
+Require FMapFacts.
 
 Require Import mathcomp.ssreflect.ssreflect.
 Require Import mathcomp.ssreflect.ssrbool.
@@ -62,7 +63,7 @@ Module NSetFacts := Facts NSet.
 Module NSetProps := Properties NSet.
 Module NSetOrdProps := OrdProperties NSet.
 
-Require Import FMapFacts.
+Import FMapFacts.
 Module NMapFacts := Facts NMap.
 
 Instance Aggregation_FailureRecorder_base_params_pt_map : BaseParamsPartialMap Aggregation_BaseParams FR.FailureRecorder_BaseParams :=
@@ -1907,6 +1908,7 @@ end; simpl.
       exact: IHH_st1.
   * have H_f := Aggregation_in_queue_fail_then_adjacent H_st1 to from H1.
     rewrite H0 in H_f.
+    simpl in *.
     concludes.
     suff H_suff: NSet.In from (adjacent (onwState net to)).
       have [m' H_ex] := Aggregation_in_set_exists_find_balance H_st1 _ H1 H_suff.

systems/FailureRecorderDynamicCorrect.v

@@ -115,7 +115,7 @@ end; simpl.
         by eauto.
       * apply: NoDup_filter_rel.
         apply: NoDup_remove_all.
-        by find_apply_lem_hyp ordered_dynamic_nodes_no_dup.
+        by apply: ordered_dynamic_nodes_no_dup; eauto.
       * apply: related_filter_rel => //.
         exact: in_remove_all_preserve.
     rewrite collate_ls_not_in; last by move => H_in; find_apply_lem_hyp filter_rel_related; break_and.
@@ -437,7 +437,7 @@ end; simpl in *.
     by eauto.
   * apply: NoDup_filter_rel.
     apply: NoDup_remove_all.
-    by find_apply_lem_hyp ordered_dynamic_nodes_no_dup.
+    by apply: ordered_dynamic_nodes_no_dup; eauto.
   * apply: related_filter_rel => //.
     exact: in_remove_all_preserve.
 - find_apply_lem_hyp net_handlers_NetHandler.
@@ -1918,6 +1918,7 @@ have H_bef := Failure_in_after_all_fail_new H_st _ H_in_n H_in_f n'.
 case (In_dec Msg_eq_dec New (odnwPackets net n' n)) => H_dec //.
 destruct (odnwPackets net n' n) => //.
 destruct m => //.
+simpl in *.
 case: H_dec => H_dec //.
 find_apply_lem_hyp in_split.
 break_exists.

systems/FailureRecorderDynamicLabeledCorrect.v

@@ -119,7 +119,7 @@ end; simpl.
         by eauto.
       * apply: NoDup_filter_rel.
         apply: NoDup_remove_all.
-        by find_apply_lem_hyp ordered_dynamic_nodes_no_dup.
+        by apply: ordered_dynamic_nodes_no_dup; eauto.
       * apply: related_filter_rel => //.
         exact: in_remove_all_preserve.
     rewrite collate_ls_not_in; last by move => H_in; find_apply_lem_hyp filter_rel_related; break_and.
@@ -441,7 +441,7 @@ end; simpl in *.
     by eauto.
   * apply: NoDup_filter_rel.
     apply: NoDup_remove_all.
-    by find_apply_lem_hyp ordered_dynamic_nodes_no_dup.
+    by apply: ordered_dynamic_nodes_no_dup; eauto.
   * apply: related_filter_rel => //.
     exact: in_remove_all_preserve.
 - find_apply_lem_hyp net_handlers_NetHandler; break_exists.
@@ -1923,6 +1923,7 @@ have H_bef := Failure_in_after_all_fail_new H_st _ H_in_n H_in_f n'.
 case (In_dec Msg_eq_dec New (odnwPackets net n' n)) => H_dec //.
 destruct (odnwPackets net n' n) => //.
 destruct m => //.
+simpl in *.
 case: H_dec => H_dec //.
 find_apply_lem_hyp in_split.
 break_exists.

systems/TreeAggregationDynamicLabeledCorrect.v

@@ -423,6 +423,7 @@ Proof.
       by admit; break_exists_name h; break_and.
     assert (~ root h)
       by admit.
+    (*
     find_eelim_prop non_root_nodes_have_unit; repeat find_rewrite; eauto.
     * intros; break_and; repeat find_rewrite.
       repeat (simpl in *; find_rewrite); find_injection.
@@ -450,6 +451,7 @@ Proof.
         [by eauto using in_remove_all_not_in|].
       find_rewrite.
       auto with datatypes.
+    *)
 Admitted.
 
 Theorem churn_free_stabilization :