proposition: Lemma composeChecksum_format_correct {P : CacheDecode -> Prop} {P_inv : (CacheDecode -> Prop) -> Prop} (decodeChecksum := decode_unused_word (sz := checksum_sz)) (P_inv_pf : cache_inv_Property P (fun P => P_inv P)) (predicate : A -> Prop) (format1 format2 : A -> CacheFormat -> Comp (B * CacheFormat)) (formatd_A_measure : B -> nat) (formatd_A_measure_OK : forall a ctx ctx' ctx'' b b' b'' ext, computes_to (format1 a ctx) (b, ctx') -> computes_to (format2 a (addE ctx' checksum_sz)) (b'', ctx'') -> predicate a -> bin_measure (mappend b (mappend (format_checksum b') b'')) = formatd_A_measure (mappend (mappend b (mappend (format_checksum b') b'')) ext)) (decodeA : B -> CacheDecode -> option (A * B * CacheDecode)) (decodeA_pf : cache_inv_Property P P_inv -> CorrectDecoder monoid predicate predicate eq (format1 ++ format_unused_word checksum_sz ++ format2) decodeA P (format1 ++ format_unused_word checksum_sz ++ format2)) (checksum_Valid_chk : forall data x x0 x1 x2 ext ext' env c, predicate data -> format1 data env ↝ (x, x0) -> format2 data (addE x0 checksum_sz) ↝ (x1, x2) -> checksum_Valid (bin_measure (mappend x (mappend (format_checksum c) x1))) (mappend (mappend x (mappend (format_checksum c) x1)) ext) -> checksum_Valid (bin_measure (mappend x (mappend (format_checksum c) x1))) (mappend (mappend x (mappend (format_checksum c) x1)) ext')) : CorrectDecoder monoid predicate predicate eq (composeChecksum format1 format2) (fun (bin : B) (env : CacheDecode) => if checksum_Valid_dec (formatd_A_measure bin) bin then decodeA bin env else None) P (composeChecksum format1 format2).
proof: Proof. unfold cache_inv_Property in *; split. { intros env env' xenv data bin ext ? env_pm pred_pm com_pf. unfold composeChecksum, Bind2 in com_pf; computes_to_inv; destruct v; destruct v0. simpl in *. find_if_inside. - intuition. assert ((format1 ++ format_unused_word checksum_sz ++ format2) data env ∋ (bin, xenv)). { unfold sequence_Format, compose. computes_to_econstructor; try eassumption; simpl. eapply refineEquiv_bind2_bind. computes_to_econstructor. + instantiate (1 := (format_checksum v1, _)). apply unfold_computes. unfold format_unused_word, Compose_Format. eexists _; split; eauto; repeat computes_to_econstructor. apply unfold_computes; eauto. + eapply refineEquiv_bind2_bind. computes_to_econstructor; eauto. eapply refineEquiv_bind2_unit. simpl; rewrite com_pf'''; eauto. } eapply H in H0; destruct_ex; split_and. rewrite H1; eexists _, _; intuition eauto. subst. unfold composeChecksum; computes_to_econstructor; eauto. computes_to_econstructor; eauto. computes_to_econstructor; eauto. simpl; rewrite <- com_pf'''; computes_to_econstructor. eauto. eauto. eauto. - destruct n. injections. erewrite <- formatd_A_measure_OK; eauto. } { intros. find_if_inside; try discriminate. - eapply decodeA_pf in H1; intuition eauto. destruct H3 as [? [? [? [? [? ?] ] ] ] ]. subst. unfold sequence_Format, compose, Bind2 in H3. computes_to_inv; subst. destruct v0; destruct v2; destruct v3; simpl in *. unfold composeChecksum, Bind2. unfold format_unused_word, Compose_Format in H3'. apply (proj1 (unfold_computes _ _)) in H3'; simpl in H3'. destruct_ex; intuition. unfold format_word in H7; computes_to_inv; injections. eexists _, _; split. computes_to_econstructor; eauto. computes_to_econstructor; simpl; eauto. computes_to_econstructor. computes_to_econstructor; simpl. intros; eapply checksum_Valid_chk. eassumption. eassumption. eassumption. erewrite formatd_A_measure_OK; eauto. computes_to_econstructor. intuition. } Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats