proposition: Lemma composeChecksum_format_correct' {P : CacheDecode -> Prop} {P_inv P_invM : (CacheDecode -> Prop) -> Prop} (decodeChecksum := decode_unused_word (sz := checksum_sz)) (P_inv_pf : cache_inv_Property P (fun P => P_inv P /\ P_invM P)) (predicate : A -> Prop) (format1 format2 : FormatM A B) (subformat : FormatM A B) (decode_measure : DecodeM (nat * B) B) (view : A -> nat -> Prop) View_Predicate view_format (decode_measure_OK : cache_inv_Property P P_invM -> CorrectRefinedDecoder monoid predicate View_Predicate view (format1 ++ format_unused_word checksum_sz ++ format2) subformat decode_measure P view_format /\ Prefix_Format _ (format1 ++ format_unused_word checksum_sz ++ format2) subformat) (view_OK : forall s v, view s v -> forall env t1 t2 (w : word checksum_sz), predicate s -> format1 s env t1 -> format2 s (addE (snd t1) checksum_sz) t2 -> bin_measure (fst t1) + (bin_measure (format_checksum w) + bin_measure (fst t2)) = v) (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) => `(n, _, _) <- decode_measure bin env; if checksum_Valid_dec n 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. specialize (decode_measure_OK (proj2 P_inv_pf)). assert ((format1 ++ format_unused_word checksum_sz ++ format2) data env ∋ (bin, xenv)). { unfold composeChecksum, sequence_Format, compose, Bind2 in *. computes_to_inv. repeat (computes_to_econstructor; try eassumption; simpl). eexists _; split; eauto; repeat computes_to_econstructor. apply unfold_computes; eauto. simpl; eauto. simpl. rewrite <- com_pf'''; computes_to_econstructor. } generalize H as H'; intro. unfold Prefix_Format in decode_measure_OK. eapply (proj2 decode_measure_OK) in H; eauto. destruct H as [? [? [? [bin_eq com_pf0] ] ] ]. destruct_ex; split_and; subst. eapply H in com_pf0; eauto. destruct_ex; split_and. rewrite <- (mappend_assoc). setoid_rewrite H4 ; simpl. simpl in *. find_if_inside. - intuition. eapply H7 in H'; destruct_ex; split_and. rewrite mappend_assoc. rewrite H10; eexists _, _; intuition eauto. subst. eauto. eauto. eauto. eauto. - destruct n. unfold composeChecksum, sequence_Format, Bind2 in com_pf; computes_to_inv; destruct v; destruct v0; injections. simpl in com_pf''. rewrite unfold_computes in H5. rewrite mappend_assoc, <- H6. rewrite unfold_computes in com_pf, com_pf'. destruct H5. eapply view_OK in H3; eauto. simpl in H3. rewrite <- H3. repeat setoid_rewrite mappend_measure in com_pf''. eauto. } { intros. destruct (decode_measure t env') as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate. find_if_inside; try discriminate. - eapply decodeA_pf in H1; intuition eauto. destruct H5 as [? [? [? [? [? ?] ] ] ] ]. rename H8 into H'. specialize (H' _ _ _ _ H5). subst. unfold sequence_Format, compose, Bind2 in H5. computes_to_inv; subst. destruct v0; destruct v2; destruct v3; simpl in *. unfold composeChecksum, Bind2. unfold format_unused_word, Compose_Format in H5'. apply (proj1 (unfold_computes _ _)) in H5'; simpl in H5'. destruct_ex; intuition. unfold format_word in H11; 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. 2: computes_to_econstructor. 2: intuition. generalize Heqo as H'; intro. eapply H7 in Heqo; eauto. split_and; destruct_ex; split_and. rewrite unfold_computes in H14. fold (format_checksum x4) in H8. rewrite <- H8 in c0. 2: rewrite <- H8; reflexivity. instantiate (1 := t'). replace (bin_measure (mappend b0 (mappend (format_checksum x4) b2))) with n. eauto. rewrite <- H8 in H'. eapply H7 in H13. destruct_ex; split_and. rewrite H8 in H'. rewrite <- mappend_assoc in H'. rewrite H16 in H'. injections. destruct H18. rewrite unfold_computes in H5; rewrite unfold_computes in H5''0. eapply view_OK in H14; eauto. rewrite <- H14. simpl. repeat setoid_rewrite mappend_measure. reflexivity. auto. auto. auto. } 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