proposition: Theorem unused_word_decode_correct {sz : nat} {S T} {monoid : Monoid T} {cache : Cache} {cacheAddNat : CacheAdd cache nat} {monoidUnit : QueueMonoidOpt monoid bool} {P : CacheDecode -> Prop} (P_OK : cache_inv_Property P (fun P => forall b cd, P cd -> P (addD cd b))) : CorrectDecoder (S := S) monoid (fun _ => True) (fun _ => True) (fun s v => True) (format_unused_word (sz := sz)) (decode_unused_word (sz := sz)) P (format_unused_word (sz := sz)).
proof: Proof. eapply format_decode_correct_alt. Focus 7. eapply injection_decode_correct with (inj := fun _ => ()). eapply Compose_decode_correct with (view := (fun _ : S => {_ : word sz | True}%comp)). eapply encode_Word_decode_correct. eapply P_OK. simpl; intros; eauto. instantiate (1 := fun _ _ => True); eauto. instantiate (1 := fun _ => True); eauto. intros. simpl in H. instantiate (1 := fun _ env t => _ env t). instantiate (1 := format_unused_word u). apply unfold_computes. unfold format_unused_word, Compose_Format; eexists v; eauto. unfold format_word, serialize, encode_word in *; intuition eauto. apply unfold_computes; eauto. - instantiate (1 := fun _ => True); unfold flip, pointwise_relation; intuition. - unfold flip, pointwise_relation; intuition. - unfold flip, pointwise_relation; intuition. - unfold flip, pointwise_relation, EquivFormat; intuition. - unfold flip, pointwise_relation; intuition. - unfold flip, pointwise_relation, EquivFormat; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats