proposition: Lemma decode_body_monotone : forall (x : B) (f g : forall y : B, lt_B y x -> CacheDecode -> option (DomainName * B * CacheDecode)), (forall (y : B) (p : lt_B y x), f y p = g y p) -> (fun cd : CacheDecode => `(labelheader, b1, env') <- Decode_w_Measure_le decode_word x cd decode_word_le; match wlt_dec WO~1~0~1~1~1~1~1~1 labelheader with | left l => `(ps, b2, env'0) <- Decode_w_Measure_le decode_word (` b1) env' decode_word_le; match getD cd (exist _ labelheader l, ps) with | Some ""%string => None | Some (String _ _ as domain) => Some (domain, ` b2, env'0) | None => None end | right r => (If wlt_dec labelheader WO~0~1~0~0~0~0~0~0 Then match weq labelheader (wzero 8) with | in_left => Some (""%string, ` b1, env') | right n => `(label, b3, env'0) <- Decode_w_Measure_lt (decode_string (wordToNat labelheader)) (` b1) env' (decode_string_lt (wordToNat labelheader) (n_eq_0_lt labelheader n)); Ifopt (index 0 "." label) as _ Then None Else ( `(domain, b4, e3) <- f (` b3) (lt_B_trans x b1 b3) env'0; If (string_dec domain "") Then Some (label, b4, Ifopt (peekD cd) as curPtr Then addD_G e3 (label, curPtr) Else e3) Else Some (label ++ (String "." domain), b4, Ifopt (peekD cd) as curPtr Then addD_G e3 (label ++ (String "." domain), curPtr) Else e3))%string end Else None) end) = (fun cd : CacheDecode => `(labelheader, b1, env') <- Decode_w_Measure_le decode_word x cd decode_word_le; match wlt_dec WO~1~0~1~1~1~1~1~1 labelheader with | left l => `(ps, b2, env'0) <- Decode_w_Measure_le decode_word (` b1) env' decode_word_le; match getD cd (exist _ _ l, ps) with | Some ""%string => None | Some (String _ _ as domain) => Some (domain, ` b2, env'0) | None => None end | right _ => (If wlt_dec labelheader WO~0~1~0~0~0~0~0~0 Then match weq labelheader (wzero 8) with | in_left => Some (""%string, ` b1, env') | right n => `(label, b3, env'0) <- Decode_w_Measure_lt (decode_string (wordToNat labelheader)) (` b1) env' (decode_string_lt (wordToNat labelheader) (n_eq_0_lt labelheader n)); Ifopt (index 0 "." label) as _ Then None Else ( `(domain, b4, e3) <- g (` b3) (lt_B_trans x b1 b3) env'0; If (string_dec domain "") Then Some (label, b4, Ifopt (peekD cd) as curPtr Then addD_G e3 (label, curPtr) Else e3) Else Some (label ++ (String "." domain), b4, Ifopt (peekD cd) as curPtr Then addD_G e3 (label ++ (String "." domain), curPtr) Else e3))%string end Else None) end).
proof: Proof. intros; apply functional_extensionality; intros. repeat (f_equal; apply functional_extensionality; intros). destruct (wlt_dec WO~1~0~1~1~1~1~1~1 x1); simpl. repeat (f_equal; apply functional_extensionality; intros). destruct (wlt_dec x1 WO~0~1~0~0~0~0~0~0); simpl. destruct (weq x1 (wzero 8)). reflexivity. repeat (f_equal; apply functional_extensionality; intros). destruct (index 0 "." x4); simpl; eauto. rewrite H; reflexivity. reflexivity. 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