proposition: Lemma refine_format_option_map sz {S S'} (g : S' -> option S) (Some_format : FormatM S _) (None_format : FormatM () _) (f : S -> word sz) (f' : word sz) (refine_Some : forall (s : S) (env : CacheFormat), refine (Some_format s env) ((format_word ◦ f) s env)) (refine_None : forall (env : CacheFormat), refine (None_format () env) ((format_word ◦ (fun _ => f')) () env)) : forall s ce, refine (FMapFormat.Projection_Format (Option.format_option Some_format None_format) g s ce) (FMapFormat.Projection_Format format_word ((fun s => Ifopt (g s) as s' Then f s' Else f')) s ce).
proof: Proof. intros; unfold FMapFormat.Projection_Format, FMapFormat.Compose_Format; intros ? ?. rewrite unfold_computes in H; destruct_ex; intuition. apply unfold_computes; eexists; split; eauto; subst. eapply refine_format_option; eauto. apply EquivFormat_Projection_Format in H0; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.BinLib Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Automation.NormalizeFormats Bedrock.Word