proposition: Lemma cache_inv_add_ptr_OK (P_OK : cache_inv_Property cache_inv (fun P => (forall env (p : pointerT) domain, P env -> getD env p = Some domain -> ValidDomainName domain /\ (String.length domain > 0)%nat) /\ (forall env p domain, P env -> (ValidDomainName domain /\ String.length domain > 0)%nat -> getD env p = None -> (forall p', peekD env = Some p' -> lt (pointerT2Nat p) (pointerT2Nat p')) -> P (addD_G env (domain, p))) /\ (forall (b : nat) (cd : CacheDecode), P cd -> P (addD cd b)) /\ (forall p (cd : CacheDecode) domain, P cd -> getD cd p = Some domain -> forall p', peekD cd = Some p' -> lt (pointerT2Nat p) (pointerT2Nat p')) )) : forall env envE p domain, cache_inv env -> Equiv envE env -> peekD env = Some p -> add_ptr_OK (domain, p) envE env.
proof: Proof. unfold cache_inv_Property, add_ptr_OK in *; simpl; intros. destruct (getD env p) eqn: ?; eauto. eapply (proj2 (proj2 (proj2 P_OK))) in Heqo; eauto. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt