proposition: Lemma PeekCacheFixpoint_Overflow : forall (n : nat) (x6 : DomainName) (xenv'' : CacheFormat) (bin' : B) (xenv0 : CacheFormat) (x9 : string) (p0 : pointerT), (forall (env : CacheFormat) (p : string) (b : nat), getE (addE env b) p = getE env p) -> (forall (env : CacheFormat) (l : string) (p p' : pointerT) (l' : string), In p (getE (addE_G env (l', p')) l) -> p = p' \/ In p (getE env l)) -> (String.length x6 <= n)%nat -> LeastFixedPoint (fun (format_DomainName : funType [DomainName; CacheFormat] (B * CacheFormat)) (domain : DomainName) (env : CacheFormat) => If string_dec domain "" Then format_ascii terminal_char env Else (position <- {position : option ({x | WO~1~0~1~1~1~1~1~1 < x} * word 8) | forall p : {x | WO~1~0~1~1~1~1~1~1 < x} * word 8, position = Some p -> In p (getE env domain)}; Ifopt position as position0 Then `(ptr1b, env') <- format_word (` (fst position0)) env; `(ptr2b, env'0) <- format_word (snd position0) env'; ret (mappend ptr1b ptr2b, env'0) Else (`(label, domain') <- {labeldomain' : string * string | (domain = (fst labeldomain' ++ String "." (snd labeldomain'))%string \/ labeldomain' = (domain, ""%string)) /\ ValidLabel (fst labeldomain') /\ (forall label' post' : string, domain = (label' ++ post')%string -> ValidLabel label' -> (String.length label' <= String.length (fst labeldomain'))%nat)}; `(lenb, env') <- format_nat 8 (String.length label) env; `(labelb, env'0) <- format_string label env'; `(domainb, env'1) <- format_DomainName domain' env'0; ret (mappend (mappend lenb labelb) domainb, Ifopt peekE env as curPtr Then addE_G env'1 (domain, curPtr) Else env'1)))) x6 xenv'' ↝ (bin', xenv0) -> peekE xenv'' = None -> peekE xenv0 = None.
proof: Proof. induction n; intros; apply (@unroll_LeastFixedPoint [DomainName; CacheFormat] (B * CacheFormat)%type _ format_body_monotone) in H2; simpl in H2. - destruct x6; simpl in *. simpl in H2; computes_to_inv. unfold format_ascii, format_word in H2; computes_to_inv; subst; simpl in *; injections. eapply addPeekENone; eauto. exfalso; omega. - destruct x6; simpl in *. + simpl in H2; computes_to_inv. unfold format_ascii, format_word in H2; computes_to_inv; subst; simpl in *; injections. eapply addPeekENone; eauto. + simpl in H2; computes_to_inv. destruct v; simpl in H2'; unfold Bind2 in *; computes_to_inv. * unfold format_word in *; computes_to_inv; subst; simpl in *; injections. eapply addPeekENone; eauto. * destruct v as [label1 label2]; destruct v0 as [b' xenv''']; destruct v1 as [b'' xenv'''']; destruct v2 as [b3 xenv5]; simpl in *; injections. generalize H2'' H2'''. apply format_nat_peekE in H2''; subst. apply format_string_peekE in H2'''; subst; intros. rewrite H3; simpl. eapply addPeekENone in H3; rewrite H3 in H2''. eapply addPeekENone in H2''; rewrite H2'' in H2'''. eapply IHn in H2''''; eauto. destruct H2' as [ [? | ?] [? ?] ]. generalize (f_equal String.length H4); simpl; rewrite !length_append; simpl; omega. injection H4; intros; subst. simpl; 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