proposition: Lemma derive_distinguishing_word v0 v1 : forall P (P_OK : cache_inv_Property P (fun P => forall b cd, P cd -> P (addD cd b))), CorrectRefinedDecoder ByteStringQueueMonoid (fun s : EthernetHeader => (ethernet_Header_OK s /\ IsProj Destination v1 s) /\ IsProj Source v0 s) (constant True) (constant (constant True)) (Either format_nat 16 ◦ constant packet_len ++ format_word ◦ constant WO~0~1~0~1~0~1~0~1 ++ format_word ◦ constant WO~0~1~0~1~0~1~0~1 ++ format_word ◦ constant WO~1~1~0~0~0~0~0~0 ++ format_word ◦ constant wzero 24 ++ format_enum EtherTypeCodes ◦ EthType ++ empty_Format Or format_enum EtherTypeCodes ◦ EthType ++ empty_Format) (format_unused_word 16) (fun t env => `(w, t', env') <- decode_word t env; if (wlt_dec w (natToWord 16 1501) : bool) then Some (true, t', env') else Some (false, t', env')) P (fun (bs : bool) (env : CacheFormat) (t : ByteString * CacheFormat) => forall (s : EthernetHeader) (t' : ByteString) (env' : CacheFormat), (fun s : EthernetHeader => (ethernet_Header_OK s /\ IsProj Destination v1 s) /\ IsProj Source v0 s) s -> ((format_nat 16 ◦ constant packet_len ++ format_word ◦ constant WO~0~1~0~1~0~1~0~1 ++ format_word ◦ constant WO~0~1~0~1~0~1~0~1 ++ format_word ◦ constant WO~1~1~0~0~0~0~0~0 ++ format_word ◦ constant wzero 24 ++ format_enum EtherTypeCodes ◦ EthType ++ empty_Format) s env (mappend (fst t) t', env') -> bs = true) /\ ((format_enum EtherTypeCodes ◦ EthType ++ empty_Format) s env (mappend (fst t) t', env') -> bs = false)).
proof: Proof. intros. apply composeIf_subformat_correct_low; intros. - unfold format_unused_word, Compose_Format in H2. rewrite unfold_computes in H2; destruct_conjs. eapply @Word_decode_correct with (P := P) in H5; eauto. destruct_conjs. rewrite H8; simpl; subst. destruct wlt_dec; simpl; eauto. - destruct decode_word as [ [ [? ?] ?] | ] eqn: ? ; simpl in H1; try discriminate. generalize Heqo; intros. eapply @Word_decode_correct with (P := P) in Heqo; try eassumption. destruct wlt_dec eqn: ?; simpl in H1; try discriminate; injections; intuition eauto 1; destruct_conjs; subst; eexists _, _; intuition eauto 1. + unfold sequence_Format, Projection_Format, Compose_Format, ComposeOpt.compose, Bind2 in H8. computes_to_inv; subst. rewrite unfold_computes in H8; destruct_conjs; subst; injections. eapply @Word_decode_correct with (P := P) in H4; try eassumption. eapply @Enum_decode_correct with (P := P) in H11; try eassumption. destruct_conjs; subst. unfold decode_enum in H19. simpl in *. rewrite <- H12 in H13. rewrite H13 in H19; simpl in H19. unfold word_indexed in H19; simpl in H19. repeat match type of H19 with context[weqb ?a ?b] => let H := fresh in destruct (weqb a b) eqn : H; try apply weqb_sound in H; subst end; simpl in H10; try discriminate. Discharge_NoDupVector. + unfold sequence_Format at 1, Projection_Format, Compose_Format, ComposeOpt.compose, Bind2 in H8. computes_to_inv; subst. clear H8'. rewrite unfold_computes in H8; destruct_conjs; subst; injections. eapply @Word_decode_correct with (P := P) in H4; try eassumption. eapply @Nat_decode_correct with (P := P) in H11; try eassumption. destruct_conjs; subst; simpl in *. unfold decode_nat in H20. rewrite <- H13 in H14. rewrite H14 in H20; simpl in H20; injections. destruct n. unfold wlt. rewrite !wordToN_nat, wordToNat_natToWord_idempotent. eapply Nomega.Nlt_in. rewrite !Nnat.Nat2N.id. eauto. reflexivity. etransitivity; try eassumption. rewrite <- Nnat.Nat2N.id. rewrite <- (Nnat.Nat2N.id 1501). apply Nomega.Nlt_out. reflexivity. Grab Existential Variables. eauto. eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Automation.NormalizeFormats Fiat.Narcissus.Automation.AlignedAutomation Bedrock.Word