Bison format enum string

src/Narcissus/Automation/AlignedAutomation.v

@@ -10,7 +10,8 @@ Require Import
         Fiat.Narcissus.Formats.StringOpt
         Fiat.Narcissus.BaseFormats
         Fiat.Narcissus.Automation.Solver
-        Fiat.Narcissus.Automation.NormalizeFormats.
+        Fiat.Narcissus.Automation.NormalizeFormats
+        Fiat.Narcissus.BinLib.AlignedString.
 
 Require Import Bedrock.Word.
 
@@ -631,6 +632,7 @@ Qed.
 (* Redefine this tactic to implement new encoder rules *)
 Ltac new_encoder_rules := fail.
 
+
 Ltac align_encoder_step :=
   first
     [ match goal with
@@ -650,7 +652,10 @@ Ltac align_encoder_step :=
     eauto using encoder_empty_cache_OK
   | apply CorrectAlignedEncoderForFormatChar; eauto
   | apply CorrectAlignedEncoderForFormatNat
+  | apply CorrectAlignedEncoderForFormatString; eauto
+  | apply CorrectAlignedEncoderFormatStringTerm; auto
   | apply CorrectAlignedEncoderForFormat2Nat; eauto
+  | apply CorrectAlignedEncoderFormatEnumString; auto
   | apply CorrectAlignedEncoderForFormatEnum
   | eapply CorrectAlignedEncoderForFormatByteBuffer; eauto using encoder_empty_cache_OK
   | eapply CorrectAlignedEncoderProjection

src/Narcissus/Automation/SynthesizeDecoder.v

@@ -33,7 +33,7 @@ Require Import
         Fiat.Narcissus.Automation.Decision
         Fiat.Narcissus.Automation.Common
         Fiat.Narcissus.Automation.ExtractData.
-
+From Coq Require Import String.
 
 Ltac shelve_inv :=
   let H' := fresh in
@@ -67,6 +67,57 @@ Ltac solve_data_inv :=
     solve [intuition eauto 3 with data_inv_hints]
     | shelve_inv ].
 
+Lemma list_ascii_of_string_app : forall s1 s2,
+    (list_ascii_of_string (s1 ++ s2))%string =
+    ((list_ascii_of_string s1) ++ (list_ascii_of_string s2))%list.
+Proof.
+  intros.
+  induction s1; auto.
+  intros.
+  simpl.
+  f_equal.
+  rewrite IHs1; auto.
+Qed.
+
+Lemma string_eq_In_list :
+  forall s s1 s2 a,
+    s = (s1 ++ String a s2)%string ->
+    In a (list_ascii_of_string s).
+Proof.
+  intros.
+  rewrite H.
+  clear H.
+  rewrite list_ascii_of_string_app.
+  apply in_or_app.               
+  right; simpl; auto.
+Qed.
+
+Ltac solve_term_char_not_in_sub :=
+  match goal with
+  | [H : In _ (list_ascii_of_string _) |- _ ] =>
+    simpl in H; solve_term_char_not_in_sub
+  | [H : _ = _ |- _ ] =>
+    inversion H; solve_term_char_not_in_sub
+  | [ H : _ \/ _ |- _ ] =>
+    destruct H; solve_term_char_not_in_sub
+  | [ H : False |- _ ]  => exact H
+  | |- _ => fail
+  end.
+
+Ltac solve_term_char_not_in :=
+  repeat
+    match goal with
+    | |- context[Vector.nth _ _ <> _] =>
+      intros; simpl; apply forall_Vector_P
+    | |- context[Vector.Forall _] =>
+      constructor
+    | |- context[_ <> _] =>
+      intros; intros Hnot;
+        apply string_eq_In_list in Hnot;
+        clear -Hnot;
+        solve solve_term_char_not_in_sub
+    end.
+
 Ltac solve_side_condition :=
   (* Try to discharge a side condition of one of the base rules *)
   match goal with
@@ -75,6 +126,8 @@ Ltac solve_side_condition :=
     let a'' := fresh in
     intro a''; intros; repeat instantiate (1 := fun _ _ => True);
     repeat destruct a'' as [ ? | a''] ; auto
+  | |- context[Vector.nth _ _ <> _] =>
+    try intros; simpl; solve_term_char_not_in
   | _ => solve [solve_data_inv]
   | _ => solve [intros; instantiate (1 := fun _ _ => True); exact I]
   end.
@@ -103,8 +156,15 @@ Ltac apply_base_rule :=
 
   (* Strings *)
   | H : cache_inv_Property _ _
-  |- context[CorrectDecoder _ _ _ _ StringOpt.format_string _ _ _ ] =>
-    eapply StringOpt.String_decode_correct
+    |- context[CorrectDecoder _ _ _ _ format_string _ _ _ ] =>
+    intros; 
+    eapply StringOpt.String_decode_correct; eauto
+
+  (* Terminated Strings *)                                              
+  | H : cache_inv_Property _ _
+    |- context[CorrectDecoder _ _ _ _ (format_string_with_term_char _) _ _ ] =>
+    intros; 
+    eapply String_decode_with_term_char_correct; eauto
 
   (* Enumerated Types *)
   | H : cache_inv_Property _ _
@@ -113,6 +173,13 @@ Ltac apply_base_rule :=
     eapply (fun NoDup => @Enum_decode_correct _ _ _ _ _ _ _ tb NoDup _ H);
     solve_side_condition
 
+  (* Enumerated Types as Strings *)
+  | H : cache_inv_Property _ _
+    |- context [CorrectDecoder _ _ _ _ (format_enum_string ?tb ?term_char) _ _ _] =>
+    intros;
+    eapply (fun NoDup => Enum_decode_string_correct _ NoDup _ _);
+    solve_side_condition
+
   (* Unused words *)
   | |- context [CorrectDecoder _  _ _ _ (format_unused_word _) _ _ _] =>
     intros; eapply unused_word_decode_correct; eauto

src/Narcissus/BinLib/AlignedDecoders.v

@@ -91,6 +91,9 @@ Section AlignedDecoders.
 
   Variable addE_addE_plus :
     forall (ce : CacheFormat) (n m : nat), addE (addE ce n) m = addE ce (n + m).
+  Variable addD_addD_plus :
+    forall (ce : CacheDecode) (n m : nat), addD (addD ce n) m = addD ce (n + m).
+
   Variable addE_0 : forall ce, addE ce 0 = ce.
   Variable addD_0 : forall cd, addD cd 0 = cd.
 
@@ -447,6 +450,60 @@ Section AlignedDecoders.
       eexists _; intuition; subst; eauto.
   Qed.
 
+  Lemma CorrectAlignedEncoderForFormatEnumString
+        {len}
+        term_char (codes : t string (S len))
+    : CorrectAlignedEncoderFor (format_enum_string codes term_char).
+  Proof with auto.
+    eexists.
+    unfold format_enum_string.
+    eapply refine_CorrectAlignedEncoder with (format' := FMapFormat.Projection_Format format_string  (fun s => (Vector.nth codes s) ++ String term_char "")%string).
+    - split; intros.
+      + unfold format_string_with_term_char, FMapFormat.Projection_Format, FMapFormat.Compose_Format.
+        intros [? ?] ?.
+        rewrite unfold_computes in H; destruct H; intuition; subst; eauto.
+      + intros.
+        intros ?; eapply H.
+        unfold format_string_with_term_char in H0;
+          unfold FMapFormat.Projection_Format, FMapFormat.Compose_Format.
+        apply unfold_computes; eexists _; eauto.
+    - eapply CorrectAlignedEncoderProjection.
+      eapply CorrectAlignedEncoderForFormatString...
+  Defined.
+
+  Definition AlignedEncoderFormatEnumString
+             {len}
+             term_char
+             (codes: t string (S len))
+    :=
+      Eval simpl in projT1 (CorrectAlignedEncoderForFormatEnumString term_char codes).
+
+  Lemma CorrectAlignedEncoderFormatEnumString
+        {len}
+        (codes : t string (S len))
+        (term_char : Ascii.ascii)
+    : CorrectAlignedEncoder
+        (format_enum_string codes term_char(monoidUnit := ByteString_QueueMonoidOpt))
+        (AlignedEncoderFormatEnumString term_char codes).
+  Proof.
+    eapply refine_CorrectAlignedEncoder.
+    2:{
+      unfold AlignedEncoderFormatEnumString.
+      eapply CorrectAlignedEncoderProjection; eauto.
+      eapply CorrectAlignedEncoderForFormatString; auto.
+    }
+    unfold format_enum_string; intros; split.
+    - intros ? ?.
+      unfold FMapFormat.Projection_Format, FMapFormat.Compose_Format in H.
+      rewrite unfold_computes in H.
+      destruct_ex; intuition; subst; eauto.
+    - intros; intro.
+      eapply H.
+      unfold FMapFormat.Projection_Format, FMapFormat.Compose_Format.
+      rewrite unfold_computes.
+      eexists _; intuition; subst; eauto.
+  Qed.
+
   Definition aligned_option_encode {S}
              (encode_Some : forall sz : nat, @AlignedEncodeM _ S sz)
              (encode_None : forall sz : nat, @AlignedEncodeM _ () sz)
@@ -1310,9 +1367,6 @@ Section AlignedDecoders.
     simpl; reflexivity.
   Qed.
 
-  Variable addD_addD_plus :
-    forall cd n m, addD (addD cd n) m = addD cd (n + m).
-
   Lemma AlignedDecodeUnusedChars {C}
         {numBytes numBytes'}
     : forall (v : ByteBuffer.t (numBytes' + numBytes))

src/Narcissus/Formats/EnumOpt.v

@@ -8,6 +8,10 @@ Require Import
         Coq.Vectors.Vector
         Bedrock.Word.
 
+Require Import Coq.Strings.String.
+Require Import Fiat.Narcissus.Formats.StringOpt.
+Require Import Fiat.Narcissus.Formats.AsciiOpt.
+
 Section Enum.
   Context {len : nat}.
   Context {A : Type}.
@@ -180,3 +184,147 @@ Ltac Discharge_NoDupVector :=
                  | inversion H]
          end
   end.
+
+Section EnumString.
+  Context {len : nat}.
+  Context {A : Type}.
+  Context {B : Type}.
+  Context {cache : Cache}.
+  Context {cacheAddNat : CacheAdd cache nat}.
+  Context {monoid : Monoid B}.
+  Context {monoidUnit : QueueMonoidOpt monoid bool}.
+
+  Context {ta : t A (S len)}.
+  Variable (tb : t string (S len)).
+
+  Definition space : Ascii.ascii
+    := Ascii.Ascii false false false false false true false false.
+
+  Definition format_enum_string (term_char : Ascii.ascii) (idx : Fin.t _) :
+    CacheFormat -> Comp (B * CacheFormat) :=
+    format_string_with_term_char term_char (nth tb idx).
+
+  Fixpoint string_indexed {n : nat}
+           (w : string)
+           (t : t string n) : option (Fin.t n)
+    := match t in Vector.t _ n return option (Fin.t n) with
+       | nil => None
+       | cons w' _ t' =>
+         if (String.eqb w w') then Some (Fin.F1) else
+           option_map Fin.FS (string_indexed w t')
+       end.
+
+  Fixpoint decode_string (s : nat) (b : B) (cd : CacheDecode) : option (string * B * CacheDecode) :=
+    match s with
+    | O => Some (EmptyString, b, cd)
+    | S s' => `(x, b1, e1) <- decode_ascii b cd;
+               if (Ascii.eqb x " ") then
+                 Some (EmptyString, b1, e1)
+               else
+               `(xs, b2, e2) <- decode_string s' b1 e1;
+                Some (String x xs, b2, e2)
+    end.
+
+  Definition decode_enum_string term_char (b : B)
+             (cd : CacheDecode)
+    : option (Fin.t _ * B * CacheDecode) :=
+    `(w, b', cd') <- (decode_string_with_term_char term_char) b cd;
+      Ifopt string_indexed w tb as idx Then
+      Some (idx, b', cd')
+      Else None.
+
+  Lemma string_indexed_correct :
+    forall n (i : Fin.t n) (t : t string n),
+      NoDupVector t
+      -> match string_indexed (nth t i) t with
+      | Some w' => i = w'
+      | None => False
+      end.
+  Proof.
+    clear.
+    induction i.
+    - intro; pattern n, t; apply Vector.caseS; simpl; intros.
+      rewrite (proj2 (String.eqb_eq h h)); eauto.
+    - intro; generalize i (IHi (Vector.tl t)); clear.
+      pattern n, t; apply Vector.caseS; simpl.
+      intros h n0 t0 i; case_eq (string_indexed (nth t0 i) t0); intros;
+        apply NoDupVector_invert in H1; intuition subst.
+      case_eq (String.eqb (nth t0 t1) h); intros; eauto.
+      apply eqb_eq in H0; subst.
+      destruct H2; generalize t0 H; clear; induction t1.
+      + intro; pattern n, t0; apply Vector.caseS; simpl; intros; econstructor.
+      + intro; revert t1 IHt1; pattern n, t0; apply Vector.caseS;
+          simpl; intros.
+        case_eq (String.eqb (nth t t1) h); intros; eauto.
+        * apply eqb_eq in H0; subst; econstructor.
+        * rewrite H0 in H.
+          econstructor 2; apply IHt1.
+          destruct (string_indexed (nth t t1) t); try discriminate.
+          f_equal.
+          unfold option_map in H.
+          apply Fin.FS_inj; congruence.
+      +
+        unfold option_map; reflexivity.
+  Qed.
+
+  Lemma string_indexed_correct':
+    forall n (v : Fin.t n) (w : string) (t : t string n),
+      string_indexed w t = Some v -> w = nth t v.
+  Proof.
+    clear.
+    induction v.
+    - intros w tb; pattern n, tb;
+        eapply Vector.caseS; simpl.
+      intros; destruct (eqb w h) eqn: ?.
+      eapply eqb_eq; eauto.
+      destruct ( string_indexed w t); try discriminate.
+    - intros w tb.
+      revert w v IHv.
+      pattern n, tb; eapply Vector.rectS; simpl; intros.
+      inversion v.
+      intros; destruct (eqb w a) eqn: ?.
+      discriminate.
+      destruct (string_indexed w v) eqn : ? ; try discriminate.
+      eapply IHv.
+      rewrite Heqo.
+      f_equal.
+      eapply Fin.FS_inj.
+      unfold option_map in H0.
+      congruence.
+  Qed.
+
+  Theorem Enum_decode_string_correct
+          (tb_OK : NoDupVector tb)
+          {P : CacheDecode -> Prop}
+          (P_OK : cache_inv_Property P (fun P => forall b cd, P cd -> P (addD cd b)))
+          term_char
+    : CorrectDecoder monoid
+                     (fun s => forall s1 s2,
+                          (nth tb s) <> s1 ++ String term_char s2)%string
+                     (fun s => forall s1 s2,
+                          (nth tb s) <> s1 ++ String term_char s2)%string
+                     eq
+                     (format_enum_string term_char)
+                     (decode_enum_string term_char) P 
+                     (format_enum_string term_char).
+  Proof.
+    unfold format_enum_string.
+    apply_bijection_rule' with (fun w => string_indexed w tb);
+      intuition eauto using String_decode_with_term_char_correct.
+    eapply string_indexed_correct in tb_OK.
+    destruct string_indexed eqn:?; subst; intuition eauto.
+    symmetry. eauto using string_indexed_correct'; eauto.
+    apply string_indexed_correct' in H0; subst; auto.
+    eapply H; eauto.
+    derive_decoder_equiv.
+    simpl.
+    unfold decode_enum_string.
+    rewrite Heqo.
+    simpl.
+    destruct (string_indexed s tb); auto.
+    unfold decode_enum_string.
+    rewrite Heqo; auto.
+  Defined.
+
+End EnumString.
+