adapt to latest cheerios and verdi-cheerios

Author: palmskog

configure

@@ -7,4 +7,5 @@ DEPS=(StructTact Verdi InfSeqExt VerdiCheerios Cheerios)
 DIRS=(lib systems extraction/aggregation/coq extraction/aggregation-dynamic/coq extraction/tree/coq extraction/tree-dynamic/coq extraction/zaggregation-dynamic/coq)
 CANARIES=("mathcomp.ssreflect.ssreflect" "Verdi Aggregation requires mathcomp to be installed" "StructTact.StructTactics" "Build StructTact before building Verdi Aggregation" "Verdi.Verdi" "Build Verdi before building Verdi Aggregation" "AAC_tactics.AAC" "Verdi Aggregation requires AAC Tactics to be installed" "InfSeqExt.infseq" "Build InfSeqExt before building Verdi Aggregation" "VerdiCheerios.SerializedParams" "Build Verdi Cheerios before building Verdi Aggregation")
 Verdi_DIRS=(core lib systems extraction)
+Cheerios_DIRS=(core extraction)
 source script/coqproject.sh

lib/BAddGroup.v

@@ -279,12 +279,21 @@ Canonical Bvector_finComRingType := Eval hnf in [finComRingType of Bvector n].
 End BitVectorRing.
 
 Require Import serializablecommfingroup.
+
 Require Import Cheerios.Cheerios.
 
 Section BitVectorSerialization.
 
 Variable n : nat.
 
+Axiom Bvector_serialize : forall (v : Bvector n), IOStreamWriter.t.
+
+Axiom Bvector_deserialize : ByteListReader.t (Bvector n).
+
+Axiom Bvector_serialize_deserialize_id :
+  serialize_deserialize_id_spec Bvector_serialize Bvector_deserialize.
+
+(*
 Definition serialize (v : Bvector n) : list bool :=
 Vector.to_list v.
 
@@ -309,9 +318,10 @@ elim => //=.
 move => b n' v IH bs.
 by rewrite IH.
 Qed.
+*)
 
 Definition Bvector_serializableMixin :=
-SerializableCommFinGroupMixin serialize_deserialize_id.
+SerializableCommFinGroupMixin Bvector_serialize_deserialize_id.
 
 Canonical Bvector_serializableCommFinGroupType :=
 SerializableCommFinGroupType (Bvector_commFinGroupType n) Bvector_serializableMixin.

lib/serializablecommfingroup.v

@@ -2,6 +2,7 @@ From mathcomp
 Require Import ssreflect ssrfun fingroup.
 
 Require Import commfingroup.
+
 Require Import Cheerios.Cheerios.
 
 Set Implicit Arguments.
@@ -13,8 +14,8 @@ Import GroupScope.
 Module SerializableCommFinGroup.
 
 Structure mixin_of (gT : commFinGroupType) := Mixin {
-  serialize : gT -> list bool ;
-  deserialize : list bool -> option (gT * list bool) ;
+  serialize : gT -> IOStreamWriter.t ;
+  deserialize : ByteListReader.t gT ;
   _ : serialize_deserialize_id_spec serialize deserialize
 }.
 
@@ -37,26 +38,18 @@ End Exports.
 End SerializableCommFinGroup.
 Export SerializableCommFinGroup.Exports.
 
-Section SerializeOps.
-
-Variable T : serializableCommFinGroupType.
-
-Definition serializeg := SerializableCommFinGroup.serialize T.
-Definition deserializeg := SerializableCommFinGroup.deserialize T.
-
-End SerializeOps.
-
 Section SerializerDefs.
 
 Variable T : serializableCommFinGroupType.
 
-Lemma serializeg_deserializeg_id : serialize_deserialize_id_spec (@serializeg T) (@deserializeg T).
+Lemma serializeg_deserializeg_id : 
+  serialize_deserialize_id_spec (SerializableCommFinGroup.serialize T) (SerializableCommFinGroup.deserialize T).
 Proof. by case: T => ? []. Qed.
 
 Global Instance FinGroupSerializer : Serializer T :=
   {
-    serialize := @serializeg T ;
-    deserialize := @deserializeg T ;
+    serialize := SerializableCommFinGroup.serialize T ;
+    deserialize := SerializableCommFinGroup.deserialize T ;
     serialize_deserialize_id := serializeg_deserializeg_id
   }.
 

systems/AggregationDynamicCorrect.v

@@ -12,11 +12,12 @@ Require Import AggregatorDynamic.
 Require Import AggregationDynamic.
 Require Import FailureRecorderDynamicCorrect.
 
+Require Import FunctionalExtensionality.
 Require Import Sumbool.
 Require Import Orders.
+Require Import Sorting.Permutation.
 Require Import MSetFacts.
 Require Import MSetProperties.
-Require Import Sorting.Permutation.
 Require FMapFacts.
 
 Require Import mathcomp.ssreflect.ssreflect.
@@ -3696,8 +3697,6 @@ end; simpl in *.
     by rewrite collate_neq.
 Qed.
 
-Require Import FunctionalExtensionality.
-
 Lemma sum_fail_map_incoming_collate_ls_filter_rel_not_in_eq :
   forall l ns h f adj map,
   ~ In h ns ->

systems/TreeAggregationDynamicSerialized.v

@@ -17,8 +17,7 @@ Require Import serializablecommfingroup.
 Require Import TreeAggregationDynamic.
 
 Require Import Cheerios.Cheerios.
-
-Require Import VerdiCheerios.SerializedParams.
+Require Import VerdiCheerios.SerializedMsgParams.
 
 Import DeserializerNotations.
 
@@ -47,25 +46,26 @@ Import TANS.
 
 Import fingroup.GroupScope.
 
-Definition option_lv_serialize (lvo : option lv) : list bool :=
+(*
+Definition option_lv_serialize (lvo : option lv) :=
 match lvo with
-| None => [false]
-| Some lv => [true] ++ serialize lv
+| None => serialize x00
+| Some lv => Serializer.append (serialize x01) (serialize lv)
 end.
 
-Definition option_lv_deserialize : deserializer (option lv) :=
+Definition option_lv_deserialize : Deserializer.t (option lv) :=
 tag <- deserialize ;;
 match tag with
-| false => ret None
-| true => Some <$> deserialize
+| x00 => Deserializer.ret None
+| x01 => Some <$> deserialize
+| _ => Deserializer.error
 end.
 
 Lemma option_lv_serialize_deserialize_id :
   serialize_deserialize_id_spec option_lv_serialize option_lv_deserialize.
 Proof.
 rewrite /option_lv_serialize /option_lv_deserialize.
-case; serialize_deserialize_id_crush.
-by rewrite /= nat_serialize_deserialize_id.
+case; repeat (cheerios_crush; simpl).
 Qed.
 
 Instance option_lv_Serialize : Serializer (option lv) :=
@@ -74,42 +74,38 @@ Instance option_lv_Serialize : Serializer (option lv) :=
     deserialize := option_lv_deserialize ;
     serialize_deserialize_id := option_lv_serialize_deserialize_id
   }.
+*)
 
-Definition Msg_serialize (msg: Msg) : list bool :=
+Definition Msg_serialize (msg: Msg) :=
   match msg with
   | Aggregate m => 
-    [false; false] ++ serialize m
-  | Fail => 
-    [false; true]
+    IOStreamWriter.append (fun _ => serialize x00) (fun _ => serialize m)
+  | Fail => serialize x01
   | Level lvo => 
-    [true; false] ++ serialize lvo
-  | New => 
-    [true; true]
+    IOStreamWriter.append (fun _ => serialize x02) (fun _ => serialize lvo)
+  | New => serialize x03
   end.
 
-Definition Msg_deserialize : deserializer Msg :=
-  tag1 <- deserialize ;;
-  tag2 <- deserialize ;;
-  match tag1, tag2 with
-  | false, false => 
+Definition Msg_deserialize : ByteListReader.t Msg :=
+  tag <- deserialize ;;
+  match tag with
+  | x00 =>
     m <- deserialize ;;
-    ret (Aggregate m)
-  | false, true => 
-    ret Fail
-  | true, false =>
+    ByteListReader.ret (Aggregate m)
+  | x01 => ByteListReader.ret Fail
+  | x02 =>
     lvo <- deserialize ;;
-    ret (Level lvo)
-  | true, true => 
-    ret New
+    ByteListReader.ret (Level lvo)
+  | x03 => ByteListReader.ret New
+  | _ => ByteListReader.error
   end.
 
 Lemma Msg_serialize_deserialize_id :
   serialize_deserialize_id_spec Msg_serialize Msg_deserialize.
 Proof.
 rewrite /Msg_serialize /Msg_deserialize.
-case; serialize_deserialize_id_crush.
-- by rewrite /= serializeg_deserializeg_id.
-- by rewrite /= option_lv_serialize_deserialize_id.
+case; repeat (cheerios_crush; simpl).
+by rewrite serializeg_deserializeg_id; cheerios_crush.
 Qed.
 
 Instance Msg_Serializer : Serializer Msg :=
@@ -119,95 +115,6 @@ Instance Msg_Serializer : Serializer Msg :=
     serialize_deserialize_id := Msg_serialize_deserialize_id
   }.
 
-Definition Input_serialize (inp : Input) : list bool :=
-  match inp with
-  | Local m => 
-    [false; false; false] ++ serialize m
-  | SendAggregate => 
-    [false; false; true]
-  | AggregateRequest s => 
-    [false; true; false] ++ serialize s
-  | LevelRequest s =>
-    [false; true; true] ++ serialize s
-  | Broadcast => 
-    [true; false; false]
-  end.
-
-Definition Input_deserialize : deserializer Input :=
-  tag1 <- deserialize ;;
-  tag2 <- deserialize ;;
-  tag3 <- deserialize ;;
-  match tag1, tag2, tag3 with
-  | false, false, false => 
-    m <- deserialize ;;
-    ret (Local m)
-  | false, false, true => 
-    ret SendAggregate
-  | false, true, false =>
-    s <- deserialize ;;
-    ret (AggregateRequest s)
-  | false, true, true =>
-    s <- deserialize ;;
-    ret (LevelRequest s)
-  | true, false, false =>
-    ret Broadcast
-  | _, _, _ => fail
-  end.
-
-Lemma Input_serialize_deserialize_id :
-  serialize_deserialize_id_spec Input_serialize Input_deserialize.
-Proof.
-rewrite /Input_serialize /Input_deserialize.
-case; serialize_deserialize_id_crush.
-- by rewrite /= serializeg_deserializeg_id.
-- by rewrite /= string_serialize_deserialize_id.
-- by rewrite /= string_serialize_deserialize_id.
-Qed.
-
-Instance Input_Serializer : Serializer Input :=
-  {
-    serialize := Input_serialize ;
-    deserialize := Input_deserialize ;
-    serialize_deserialize_id := Input_serialize_deserialize_id
-  }.
-
-Definition Output_serialize (out : Output) : list bool :=
-  match out with
-  | AggregateResponse s m => 
-    [false] ++ serialize s ++ serialize m
-  | LevelResponse s lvo => 
-    [true] ++ serialize s ++ serialize lvo
-  end.
-
-Definition Output_deserialize : deserializer Output :=
-  tag <- deserialize ;;
-  match tag with
-  | false =>
-    s <- deserialize ;;
-    m <- deserialize ;;
-    ret (AggregateResponse s m)
-  | true =>
-    s <- deserialize ;;
-    lvo <- deserialize ;;
-    ret (LevelResponse s lvo)
-  end.
-
-Lemma Output_serialize_deserialize_id :
-  serialize_deserialize_id_spec Output_serialize Output_deserialize.
-Proof.
-rewrite /Output_serialize /Output_deserialize.
-case; serialize_deserialize_id_crush.
-- by rewrite /= string_serialize_deserialize_id serializeg_deserializeg_id.
-- by rewrite /= string_serialize_deserialize_id option_lv_serialize_deserialize_id.
-Qed.
-
-Instance Output_Serializer : Serializer Output :=
-  {
-    serialize := Output_serialize ;
-    deserialize := Output_deserialize ;
-    serialize_deserialize_id := Output_serialize_deserialize_id
-  }.
-
 Definition TreeAggregation_SerializedBaseParams :=
 serialized_base_params.