proposition: Lemma format_word_is_encode_word {T} {cache : Cache} {cacheAddNat : CacheAdd cache nat} {monoid : Monoid T} {monoidUnit : QueueMonoidOpt monoid bool} {n} (enc : EncodeM (word n) T) : (forall s env, (forall t env', enc s env = Some (t, env') -> refine (format_word s env) (ret (t, env'))) /\ (enc s env = None -> forall benv', ~ computes_to (format_word s env) benv')) -> forall s env, enc s env = Some (encode_word' _ s mempty, addE env n).
proof: Proof. intros. destruct enc eqn:?; destruct_conjs. - apply H in Heqe. eapply Return_inv in Heqe; eauto. congruence. - exfalso. eapply H; eauto. computes_to_econstructor; 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.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad 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 Bedrock.Word