proposition: Theorem SumType_decode_correct {m} {P} (types : Vector.t Type m) (formatrs : ilist (B := fun T => T -> CacheFormat -> Comp (B * CacheFormat)) types) (decoders : ilist (B := fun T => B -> CacheDecode -> option (T * B * CacheDecode)) types) (invariants : ilist (B := fun T => Ensemble T) types) (cache_invariants : Vector.t (Ensemble (CacheDecode -> Prop)) m) (formatrs_decoders_correct : Iterate_Ensemble_BoundedIndex (fun idx => cache_inv_Property P (Vector.nth cache_invariants idx) -> CorrectDecoder monoid (ith invariants idx) (ith invariants idx) eq (ith formatrs idx) (ith decoders idx) P (ith formatrs idx))) idx : cache_inv_Property P (fun P => Iterate_Ensemble_BoundedIndex (fun idx => Vector.nth cache_invariants idx P)) -> CorrectDecoder monoid (fun st => SumType_index types st = idx /\ (ith invariants) _ (SumType_proj types st)) (fun st => SumType_index types st = idx /\ (ith invariants) _ (SumType_proj types st)) eq (format_SumType types formatrs) (decode_SumType types decoders idx) P (format_SumType types formatrs).
proof: Proof. intros; eapply SumType_decode_correct'; eauto. intros. eapply Iterate_Ensemble_BoundedIndex_equiv in formatrs_decoders_correct; eauto. unfold cache_inv_Property in *; intros; eapply Iterate_Ensemble_BoundedIndex_equiv in H; eauto. Qed.
imports: Fiat.Common.ilist Fiat.Common.SumType Fiat.Common.IterateBoundedIndex Fiat.Narcissus.Common.Specs Coq.Sets.Ensembles Bedrock.Word