proposition: Lemma distinguishing_word_prefix : Prefix_Format _ (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).
proof: Proof. unfold Prefix_Format, composeIf, Union_Format; intros. rewrite unfold_computes in H. destruct_ex; revert H; pattern x; apply IterateBoundedIndex.Iterate_Ensemble_BoundedIndex_equiv; simpl; econstructor; [intros | econstructor; intros; eauto]. Opaque natToWord. + unfold Vector.nth in H; simpl in H. unfold sequence_Format at 1 in H. unfold Projection_Format, empty_Format, Compose_Format, ComposeOpt.compose, Bind2 in H. computes_to_inv. rewrite unfold_computes in H; destruct_ex; split_and; subst; eauto. unfold format_nat, format_word in H0; computes_to_inv; subst. injections; eexists _, _, _; intuition eauto. unfold format_unused_word, Compose_Format. apply unfold_computes; eexists _; intuition eauto; try computes_to_econstructor. apply unfold_computes; eauto. + unfold Vector.nth in H; simpl in H. unfold sequence_Format at 1 in H. unfold Projection_Format, empty_Format, Compose_Format, ComposeOpt.compose, Bind2 in H. computes_to_inv. rewrite unfold_computes in H; destruct_ex; split_and; subst; eauto. unfold format_enum, format_word in H0; computes_to_inv; subst. injections; eexists _, _, _; intuition eauto. unfold format_unused_word, Compose_Format. apply unfold_computes; eexists _; intuition eauto; try computes_to_econstructor. apply unfold_computes; 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