From 04cb8f48b9c29aba7b3c40ac0da54efba153beda Mon Sep 17 00:00:00 2001 From: "Nathan St. Amour" Date: Mon, 3 Jan 2022 16:53:39 -0500 Subject: [PATCH 1/8] Encoders/Decoders for enums that encode strings as codes --- src/Narcissus/BinLib/AlignedDecoders.v | 57 ++++++++++ src/Narcissus/Formats/EnumOpt.v | 148 +++++++++++++++++++++++++ 2 files changed, 205 insertions(+) diff --git a/src/Narcissus/BinLib/AlignedDecoders.v b/src/Narcissus/BinLib/AlignedDecoders.v index 88c9ff719..eada8b702 100644 --- a/src/Narcissus/BinLib/AlignedDecoders.v +++ b/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) diff --git a/src/Narcissus/Formats/EnumOpt.v b/src/Narcissus/Formats/EnumOpt.v index 1789e37ca..bfb8e6e8a 100644 --- a/src/Narcissus/Formats/EnumOpt.v +++ b/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. + From d429736f795a8f096ba5bf86d58b69fc33e4a09a Mon Sep 17 00:00:00 2001 From: "Nathan St. Amour" Date: Tue, 4 Jan 2022 12:09:05 -0500 Subject: [PATCH 2/8] Duplicate variable declared --- src/Narcissus/BinLib/AlignedDecoders.v | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Narcissus/BinLib/AlignedDecoders.v b/src/Narcissus/BinLib/AlignedDecoders.v index eada8b702..2d571ad23 100644 --- a/src/Narcissus/BinLib/AlignedDecoders.v +++ b/src/Narcissus/BinLib/AlignedDecoders.v @@ -1367,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)) From a0532e37582fc7e3ddec7355618feadff28d6e8e Mon Sep 17 00:00:00 2001 From: "Nathan St. Amour" Date: Tue, 4 Jan 2022 14:14:18 -0500 Subject: [PATCH 3/8] Rule for format_enum_string CorrectDecoder in apply_base_rule --- src/Narcissus/Automation/SynthesizeDecoder.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Narcissus/Automation/SynthesizeDecoder.v b/src/Narcissus/Automation/SynthesizeDecoder.v index 63dc41f11..83bc4a4b3 100644 --- a/src/Narcissus/Automation/SynthesizeDecoder.v +++ b/src/Narcissus/Automation/SynthesizeDecoder.v @@ -113,6 +113,12 @@ 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 _ _) + (* Unused words *) | |- context [CorrectDecoder _ _ _ _ (format_unused_word _) _ _ _] => intros; eapply unused_word_decode_correct; eauto From 80862abcfa02d6a53b7dd96db829c66fea6e185f Mon Sep 17 00:00:00 2001 From: "Nathan St. Amour" Date: Tue, 4 Jan 2022 14:29:34 -0500 Subject: [PATCH 4/8] align_encoder_step for format_enum_string --- src/Narcissus/Automation/AlignedAutomation.v | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Narcissus/Automation/AlignedAutomation.v b/src/Narcissus/Automation/AlignedAutomation.v index 620af24a5..69bab67bd 100644 --- a/src/Narcissus/Automation/AlignedAutomation.v +++ b/src/Narcissus/Automation/AlignedAutomation.v @@ -651,6 +651,7 @@ Ltac align_encoder_step := | apply CorrectAlignedEncoderForFormatChar; eauto | apply CorrectAlignedEncoderForFormatNat | apply CorrectAlignedEncoderForFormat2Nat; eauto + | apply CorrectAlignedEncoderFormatEnumString; auto | apply CorrectAlignedEncoderForFormatEnum | eapply CorrectAlignedEncoderForFormatByteBuffer; eauto using encoder_empty_cache_OK | eapply CorrectAlignedEncoderProjection From f16467f8e0f9c953ddd2d4b27c402499c5985541 Mon Sep 17 00:00:00 2001 From: "Nathan St. Amour" Date: Tue, 4 Jan 2022 15:42:35 -0500 Subject: [PATCH 5/8] solve_side_condition automation for format_enum_string --- src/Narcissus/Automation/SynthesizeDecoder.v | 40 +++++++++++++++++++- 1 file changed, 38 insertions(+), 2 deletions(-) diff --git a/src/Narcissus/Automation/SynthesizeDecoder.v b/src/Narcissus/Automation/SynthesizeDecoder.v index 83bc4a4b3..f0ebb78ba 100644 --- a/src/Narcissus/Automation/SynthesizeDecoder.v +++ b/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,39 @@ 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 := + simpl; + apply forall_Vector_P; + repeat constructor; + (intros s1 s2 Hnot; + apply string_eq_In_list in Hnot; + destruct Hnot as [Hnot | Hnot']; [|destruct Hnot']; auto; discriminate). + Ltac solve_side_condition := (* Try to discharge a side condition of one of the base rules *) match goal with @@ -75,6 +108,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. @@ -117,7 +152,8 @@ Ltac apply_base_rule := | H : cache_inv_Property _ _ |- context [CorrectDecoder _ _ _ _ (format_enum_string ?tb ?term_char) _ _ _] => intros; - eapply (fun NoDup => Enum_decode_string_correct _ NoDup _ _) + eapply (fun NoDup => Enum_decode_string_correct _ NoDup _ _); + solve_side_condition (* Unused words *) | |- context [CorrectDecoder _ _ _ _ (format_unused_word _) _ _ _] => From 76a29280585315d48ca52e2803c4e2eb09aa2a39 Mon Sep 17 00:00:00 2001 From: "Nathan St. Amour" Date: Tue, 4 Jan 2022 16:22:19 -0500 Subject: [PATCH 6/8] Made Vector.nth side condition solving more general --- src/Narcissus/Automation/SynthesizeDecoder.v | 30 ++++++++++++++++---- 1 file changed, 24 insertions(+), 6 deletions(-) diff --git a/src/Narcissus/Automation/SynthesizeDecoder.v b/src/Narcissus/Automation/SynthesizeDecoder.v index f0ebb78ba..71407e437 100644 --- a/src/Narcissus/Automation/SynthesizeDecoder.v +++ b/src/Narcissus/Automation/SynthesizeDecoder.v @@ -92,13 +92,31 @@ Proof. 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 := - simpl; - apply forall_Vector_P; - repeat constructor; - (intros s1 s2 Hnot; - apply string_eq_In_list in Hnot; - destruct Hnot as [Hnot | Hnot']; [|destruct Hnot']; auto; discriminate). + 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 *) From ea65e334be9c4e94ab7b0f2a258a08e76894b625 Mon Sep 17 00:00:00 2001 From: "Nathan St. Amour" Date: Tue, 4 Jan 2022 17:17:40 -0500 Subject: [PATCH 7/8] Partial automation tactic fixes for format_string variants --- src/Narcissus/Automation/AlignedAutomation.v | 2 ++ src/Narcissus/Automation/SynthesizeDecoder.v | 11 +++++++++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/Narcissus/Automation/AlignedAutomation.v b/src/Narcissus/Automation/AlignedAutomation.v index 69bab67bd..6ed3fffae 100644 --- a/src/Narcissus/Automation/AlignedAutomation.v +++ b/src/Narcissus/Automation/AlignedAutomation.v @@ -650,6 +650,8 @@ 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 diff --git a/src/Narcissus/Automation/SynthesizeDecoder.v b/src/Narcissus/Automation/SynthesizeDecoder.v index 71407e437..67e62b0bd 100644 --- a/src/Narcissus/Automation/SynthesizeDecoder.v +++ b/src/Narcissus/Automation/SynthesizeDecoder.v @@ -156,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 _ _ From c709a3c1b59d9d14e8801afd1645c63127dae9af Mon Sep 17 00:00:00 2001 From: "Nathan St. Amour" Date: Mon, 10 Jan 2022 16:47:02 -0500 Subject: [PATCH 8/8] Missing include --- src/Narcissus/Automation/AlignedAutomation.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Narcissus/Automation/AlignedAutomation.v b/src/Narcissus/Automation/AlignedAutomation.v index 6ed3fffae..0ca7736a1 100644 --- a/src/Narcissus/Automation/AlignedAutomation.v +++ b/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