proposition: Lemma CorrectAlignedEncoderForFormatEnum {len} (codes : t (word 8) (S len)) : CorrectAlignedEncoder (format_enum codes (monoidUnit := ByteString_QueueMonoidOpt)) (fun sz v idx n => @SetCurrentByte _ _ sz v idx (Vector.nth codes n)).
proof: Proof. eapply refine_CorrectAlignedEncoder. 2: eapply CorrectAlignedEncoderForFormatChar_f; eauto. unfold format_enum; 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.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word