text:
Require Import List Omega Numbers.BinNums Psatz.
Import List.ListNotations.

Require Import Cecoa.Lib Cecoa.Interface.

Inductive variable := x | y | p | q | x0 | m | c | n' | m' | r | r'.
Inductive function := pred_doubleF | succ_double_maskF | double_maskF | double_pred_maskF | sub_maskF | sub_mask_carryF | compare_contEqF | compare_contGtF | compare_contLtF | compareF | succ_doubleF | doubleF | subF | compare0F | lebF | moduloF | errF | sub_auxF | leb_auxF | pos_moduloOF | pos_moduloIF | pos_moduloF | condF | succF | addF | add_carryF | add0F | mul_modF | mul_mod_auxF | exp_modF | exp_mod_auxF | mod_auxF | modF | boundF.
Inductive constructor := TrueC | FalseC | PairC | EqC | LtC | GtC | XIC | XOC | XHC | N0C | NposC | IsNulC | IsPosC | IsNegC | errC.

Scheme Equality for variable.
Scheme Equality for constructor.
Scheme Equality for function.

Module EMSyntax <: Interface.SYNTAX.
  Definition variable := variable.
  Definition function := function.
  Definition constructor := constructor.

  Definition function_default := errF.
  Definition constructor_default := errC.

  Definition variable_eq_dec := variable_eq_dec.
  Definition function_eq_dec := function_eq_dec.
  Definition constructor_eq_dec := constructor_eq_dec.
End EMSyntax.

Module Import Syn := Interface.MkSyn(EMSyntax).
Import Syn.ProgramNotations.

Definition var_coercion : variable -> term := var_coercion_gen.
Coercion var_coercion : variable >-> term.
Notation " x '#' l " := (capply x (map var_coercion l)) (at level 50).

(* Some notations for the constructors *)
Notation "'XO' a" := (capply XOC [var_coercion a]) (at level 60).
Notation "'XI' a" := (capply XIC [var_coercion a]) (at level 60).
Notation "'Ispos' a" := (capply IsPosC [var_coercion a]) (at level 60).
Notation "'NPos' a" := (capply NposC [var_coercion a]) (at level 60).
Notation "'XH'" := (capply XHC []) (at level 60).
Notation "'Isnul'" := (capply IsNulC []) (at level 60).
Notation "'Isneg'" := (capply IsNegC []) (at level 60).
Notation "'GT'" := (capply GtC []) (at level 60).
Notation "'LT'" := (capply LtC []) (at level 60).
Notation "'EQ'" := (capply EqC []) (at level 60).
Notation "'N0'" := (capply N0C []) (at level 60).
Notation "'TRUE'" := (capply TrueC []) (at level 60).
Notation "'FALSE'" := (capply FalseC []) (at level 60).

(* Mostly generated using:
Extraction Language Haskell.
Recursive Extraction N.modulo.*)

Definition em_prog : list rule := [
pred_doubleF (: XI p :) --> capply XIC [XO p];
pred_doubleF (: XO p :) --> capply XIC [pred_doubleF (: p :)];
pred_doubleF (: XH :) --> XH;

succ_double_maskF (: Isnul :) --> capply IsPosC [XH];
succ_double_maskF (: Ispos p :)  --> capply IsPosC [XI p];
succ_double_maskF (: Isneg :) --> Isneg;

double_maskF (: Ispos p :) --> capply IsPosC [XO p];
double_maskF (: x0 :) --> x0;

double_pred_maskF (: XI p :) -->
  capply IsPosC [capply XOC [XO p]];
double_pred_maskF (: XO p :) -->
  capply IsPosC [capply XOC [pred_doubleF (: p :)]];
double_pred_maskF (: XH :) --> Isnul;

sub_maskF (: XI p, XI q :) --> double_maskF (: sub_maskF (: p, q :) :);
sub_maskF (: XI p, XO q :) --> succ_double_maskF (: sub_maskF (: p, q :) :);
sub_maskF (: XI p, XH :) --> capply IsPosC [XO p];

sub_maskF (: XO p, XI q :) -->
  succ_double_maskF (: sub_mask_carryF (: p, q :) :);
sub_maskF (: XO p, XO q :) --> double_maskF (: sub_maskF (: p, q :) :);
sub_maskF (: XO p, XH :) --> capply IsPosC [pred_doubleF (: p :)];
sub_maskF (: XH, XH :) --> Isnul;
sub_maskF (: XH, q :) --> Isneg;

sub_mask_carryF (: XI p, XI q :) -->
  succ_double_maskF (: sub_mask_carryF (: p, q :) :);
sub_mask_carryF (: XI p, XO q :) -->
  double_maskF (: sub_maskF (: p, q :) :);
sub_mask_carryF (: XI p, XH :) --> capply IsPosC [pred_doubleF (: p :)];
sub_mask_carryF (: XO p, XI q :) -->
  double_maskF (: sub_mask_carryF (: p, q :) :);
sub_mask_carryF (: XO p, XO q :) -->
  succ_double_maskF (: sub_mask_carryF (: p, q :) :);
sub_mask_carryF (: XO p, XH :) --> double_pred_maskF (: p :);
sub_mask_carryF (: XH, q :) --> Isneg;

(* compare_cont with r specified, to have ppo *)
compare_contEqF (: XI p, XI q :) --> compare_contEqF (: p, q :);
compare_contEqF (: XI p, XO q :) --> compare_contGtF (: p, q :);
compare_contEqF (: XI p, XH :) --> GT;
compare_contEqF (: XO p, XI q :) --> compare_contLtF (: p, q :);
compare_contEqF (: XO p, XO q :) --> compare_contEqF (: p, q :);
compare_contEqF (: XO p, XH :) --> GT;
compare_contEqF (: XH, XH :) --> EQ;
compare_contEqF (: XH, q :) --> LT;

compare_contLtF (: XI p, XI q :) --> compare_contLtF (: p, q :);
compare_contLtF (: XI p, XO q :) --> compare_contGtF (: p, q :);
compare_contLtF (: XI p, XH :) --> GT;
compare_contLtF (: XO p, XI q :) --> compare_contLtF (: p, q :);
compare_contLtF (: XO p, XO q :) --> compare_contLtF (: p, q :);
compare_contLtF (: XO p, XH :) --> GT;
compare_contLtF (: XH, XH :) --> LT;
compare_contLtF (: XH, q :) --> LT;

compare_contGtF (: XI p, XI q :) --> compare_contGtF (: p, q :);
compare_contGtF (: XI p, XO q :) --> compare_contGtF (: p, q :);
compare_contGtF (: XI p, XH :) --> GT;
compare_contGtF (: XO p, XI q :) --> compare_contLtF (: p, q :);
compare_contGtF (: XO p, XO q :) --> compare_contGtF (: p, q :);
compare_contGtF (: XO p, XH :) --> GT;
compare_contGtF (: XH, XH :) --> GT;
compare_contGtF (: XH, q :) --> LT;

compareF (: p, q :) -->  compare_contEqF (: p, q :);

succ_doubleF (: N0 :) --> capply NposC [XH];
succ_doubleF (: NPos p :) --> capply NposC [XI p];

doubleF (: N0 :) --> N0;
doubleF (: NPos p :) --> capply NposC [XO p];

(* added for case *)
sub_auxF (: Ispos p :) --> NPos p;
sub_auxF (: p :) --> N0;

subF (: N0, m :) --> N0;
subF (: NPos p, N0 :) --> NPos p;
subF (: NPos p, NPos q :) --> sub_auxF (: sub_maskF (: p, q :) :);

compare0F (: N0, N0 :) --> EQ;
compare0F (: N0, NPos q :) --> LT;
compare0F (: NPos n', N0 :) --> GT;
compare0F (: NPos n', NPos m' :) --> compareF (: n', m' :);

leb_auxF (: GT :) --> FALSE;
leb_auxF (: q :) --> TRUE;

lebF (:x, y :) --> leb_auxF (: compare0F (: x, y :) :);

condF (: TRUE, x, y :) --> x;
condF (: FALSE, x, y :) --> y;

mod_auxF (: XH, capply NposC [XH] :) --> N0 ;
mod_auxF (: XH, m :) --> capply NposC [XH] ;
mod_auxF (: XO x, m :) -->
  condF (: lebF (: m, doubleF (: mod_auxF (: x, m :) :) :),
           subF (: doubleF (: mod_auxF (: x, m :) :), m :),
           doubleF (: mod_auxF (: x, m :) :) :) ;
mod_auxF (: XI x, m :) -->
  condF (: lebF (: m, succ_doubleF (: mod_auxF (: x, m :) :) :),
           subF (: succ_doubleF (: mod_auxF (: x, m :):), m :),
           succ_doubleF (: mod_auxF (: x, m :) :) :) ;

modF (: N0, m :) --> N0;
modF (: NPos x, m :) --> mod_auxF (: x, m :);

(* back to extracted code *)

succF (: XI p :) --> capply XOC [succF (: p :)];
succF (: XO p :) --> XI p;
succF (: XH :) --> capply XOC [XH];

addF (: XI p, XI q :) --> capply XOC [add_carryF (: p, q :)];
addF (: XI p, XO q :) --> capply XIC [addF (: p, q :)];
addF (: XI p, XH :) --> capply XOC [succF (: p :)];
addF (: XO p, XI q :) --> capply XIC [addF (: p, q :)];
addF (: XO p, XO q :) --> capply XOC [addF (: p, q :)];
addF (: XO p, XH :) --> XI p;
addF (: XH, XI q :) --> capply XOC [succF (: q :)];
addF (: XH, XO q :) --> XI q;
addF (: XH, XH :) --> capply XOC [XH];

add_carryF (: XI p, XI q :) --> capply XIC [add_carryF (: p, q :)];
add_carryF (: XI p, XO q :) --> capply XOC [add_carryF (: p, q :)];
add_carryF (: XI p, XH :) --> capply XIC [succF (: p :)];
add_carryF (: XO p, XI q :) --> capply XOC [add_carryF (: p, q :)];
add_carryF (: XO p, XO q :) --> capply XIC [addF (: p, q :)];
add_carryF (: XO p, XH :) --> capply XOC [succF (: p :)];
add_carryF (: XH, XI q :) --> capply XIC [succF (: q :)];
add_carryF (: XH, XO q :) --> capply XOC [succF (: q :)];
add_carryF (: XH, XH :) --> capply XIC [XH];

add0F (: N0, m :) --> m;
add0F (: NPos p, N0 :) --> NPos p;
add0F (: NPos p, NPos q :)--> capply NposC [addF (: p, q :)];

mul_mod_auxF (: XI p, y, m, XO x :) -->
  modF (: add0F (: y, doubleF (: mul_mod_auxF (: p, y, m, x :) :):), m :);
mul_mod_auxF (: XO p, y, m, XO x :) -->
  modF (: doubleF (: mul_mod_auxF (: p, y, m, x :) :), m :);
mul_mod_auxF (: XH, y, m, x :) --> modF (: y, m :);

mul_modF (: N0, y, m, p :) --> N0;
mul_modF (: NPos x , y, m, p :) --> mul_mod_auxF (: x, y, m, p :);

exp_mod_auxF (: x, XH, m, p :) --> modF (: x, m :);
exp_mod_auxF (: x, XO y, m, p :) -->
  mul_modF (: exp_mod_auxF (: x, y, m, p :), exp_mod_auxF (: x, y, m, p :), m, p :) ;
exp_mod_auxF (: x, XI y, m, p :) -->
  mul_modF (: modF (: x, m :), mul_modF (: exp_mod_auxF (: x, y, m, p :), exp_mod_auxF (: x, y, m, p :), m, p :), m, p :);

boundF (: N0 :) --> XH;
boundF (: NPos p :) --> boundF (: p :);
boundF (: XH :) --> capply XOC [XH];
boundF (: XI x :) --> capply XOC [boundF (: x :)];
boundF (: XO x :) --> capply XOC [boundF (: x :)];

exp_modF (: x, N0 , m :) --> modF(: capply NposC [XH], m :) ;
exp_modF (: x, NPos y, m :) --> exp_mod_auxF (: x, y, m, boundF (: m :) :)
].

Module EMProg <: Syn.PROGRAM.
  Definition prog := em_prog.
End EMProg.

Module Import Prog := Syn.MkProg (EMProg).
Import Prog.QI Prog.Evaluator.

Definition rank : function -> nat := ltac:(autorank function_beq ranklist).

(* It's a program *)
Proposition Expmod_is_wf: wf_prog.
Proof. cbv; repeat split; try tauto; auto. Qed.

Proposition expmod_is_ppo : PPO_prog rank.
Proof.
  cbv.
  intros r H.
  decompose sum H; subst; ppo.
Qed.

(* QI *)
Definition cs (c : constructor) := 1%nat. (* same for all *)

Lemma qic_nonzero : constructor_non_zero cs.
Proof. cbv; auto. Qed.

Definition mcs := 1.
Lemma qic_bounded : mcs_is_max_constructor_size mcs cs.
Proof. cbv; auto. Qed.

Definition qic (c : constructor) args := suml args + cs c.

Lemma qic_additivity : additive qic cs.
Proof. cbv; auto. Qed.

Lemma cons_app {A : Type}  (h: A) t: h::t = [h] ++t.
Proof. trivial. Qed.

(* big tactic hopefully proving inequalities *)
Ltac try_prove_ineq :=
unfold qic, cs;
try tauto; intros; subst; cbn; try omega;
repeat rewrite Nat.add_0_r; repeat rewrite Nat.max_0_r;
repeat rewrite Nat.add_max_distr_r; repeat rewrite Nat.add_1_r;
repeat rewrite Nat.max_id, Max.max_r;
try (solve [simpl; auto with *]);
try (nia); repeat (case QI.value_assignment); auto with *.

(* tactic proving 1 inequality *)
Ltac prove_rule H :=
  rewrite cons_app; apply QI.p_smc_QI_app;
  [ intros f lp t s; cbn; intro H;
    repeat (destruct H as [ H | H ];
      [inversion H; subst; unfold map; simpl;
       repeat rewrite QI.value_as_p_term_assignment;
        eexists; eexists; repeat split; repeat try_prove_ineq| ]); inversion H
  |].

Definition spec_QI (f : function) (qf : list nat -> nat) :=
 fun g => if function_beq g f then Some qf else None.

Ltac inst f qi := idtac "instantiating" f; apply QI.p_smc_split with (h := spec_QI f qi).

(* get next function name and instantiate it *)
Ltac inst_next qi :=
match goal with
| |- context[rulify (Syntax.fapply ?ff _) _ ::_] =>
    (idtac "instantiating" ff;
    apply QI.p_smc_split with (h := spec_QI ff qi))
end.

Ltac qif_monotonic_tac :=
  repeat (apply forall2_le_suml || apply forall2_le_maxl ||
          apply Plus.plus_le_compat_r || apply Plus.plus_le_compat_l || apply Plus.plus_le_compat ||
          apply Nat.max_le_compat_r || apply Nat.max_le_compat_l || apply Nat.max_le_compat ||
          apply Mult.mult_le_compat_l || apply Mult.mult_le_compat_r || apply Mult.mult_le_compat
         ); trivial.

Definition qif_proofs : {qif | subterm qif /\ monotonicity_qif qif /\ compatible_QI qic qif}.
Proof.
(* let's define the qi via a partial function, starting with an
   everywhere undefined function *)
apply QI.p_smc_smc.
unfold EMProg.prog, em_prog.

inst_next (fun x => maxl x + 1). do 3 (prove_rule H).

inst_next (fun x => maxl x + 1).
inst double_maskF (fun x => maxl x + 1).
do 5 (prove_rule H).

inst_next (fun x => maxl x + 2).
inst sub_maskF (fun x => maxl x + 1).
inst sub_mask_carryF (fun x => maxl x + 1).
do 18 (prove_rule H).

inst_next maxl.
inst compare_contLtF maxl.
inst compare_contGtF maxl.
inst compareF maxl.
do 25 (prove_rule H).

inst_next (fun l => maxl l + 1).
inst doubleF (fun l => maxl l + 1).
do 4 (prove_rule H).

inst_next (fun l => maxl l). prove_rule H.
(* second rule relies on constructor_non_zero *)
rewrite cons_app. apply QI.p_smc_QI_app.
{ intros f lp t s. cbn. intro H.
  destruct H; try tauto. inversion H.
  subst. unfold map. simpl.
  rewrite QI.value_as_p_term_assignment. simpl.
  eexists. eexists. repeat split; auto.
  rewrite Nat.max_0_r.
  unfold qic at 1. simpl. unfold cs.
  apply le_trans with (m:=Syntax.value_size (s p)).
  - rewrite <- Syntax.compatible_sizes with (variable:=variable) (function:=function).
    set (v:=Syntax.term_from_value variable function (s p)).
    generalize (Syntax.gt_term_size_O v). intro. omega.
  - apply QI.value_size_le_QI with (cs:=cs).
    + apply qic_additivity.
    + apply qic_nonzero.
}
inst_next (fun l => maxl l).
do 3 (prove_rule H).

inst_next maxl. do 4 (prove_rule H).

inst_next (fun l => maxl l). prove_rule H.
(* second rule relies on constructor_non_zero *)
rewrite cons_app. apply QI.p_smc_QI_app.
{ intros f lp t s. cbn. intro H.
  destruct H; try tauto. inversion H.
  subst. unfold map. simpl.
  rewrite QI.value_as_p_term_assignment. simpl.
  eexists. eexists. repeat split; auto.
  rewrite Nat.max_0_r.
  unfold qic at 1. simpl. unfold cs.
  apply le_trans with (m:=Syntax.value_size (s q)).
  - rewrite <- Syntax.compatible_sizes with (variable:=variable) (function:=function).
    set (v:=Syntax.term_from_value variable function (s q)).
    generalize (Syntax.gt_term_size_O v). intro. omega.
  - apply QI.value_size_le_QI with (cs:=cs).
    + apply qic_additivity.
    + apply qic_nonzero.
}

inst_next maxl. prove_rule H.

inst_next maxl. do 2 (prove_rule H).

(* modF *)
inst_next (fun l => suml l + 1). do 4 (prove_rule H).
inst_next (fun l => suml l + 1). do 2 (prove_rule H).

inst_next (fun l => maxl l + 1); do 3 (prove_rule H).
inst add_carryF (fun l => maxl l + 1).
inst_next (fun l => maxl l + 1). do 18 (prove_rule H).

inst_next (fun l => maxl l + 1); do 3 (prove_rule H).

inst_next (fun l => match l with [p1;y1;m1;c1] => (m1+3) * (c1+1) + max p1 y1 | _ => maxl l end).
do 3 (prove_rule H).

inst_next (fun l => match l with [p1;y1;m1;c1] => (m1+3) * (c1+1) + max p1 y1 | _ => maxl l end).
do 2 (prove_rule H).

inst_next (fun l => match l with [x1;y1;m1;c1] =>
  x1 + (y1 + 1) * 2 * (m1+3) * (c1+1) | _ => maxl l end).
do 3 (prove_rule H).

(* bound *)
inst_next (fun l => maxl l +1).
do 5 (prove_rule H).

(* expmod *)
(* (y1+1) because of subterm *)
inst_next (fun l => match l with [x1;y1;m1] =>
  x1 + (y1+1) * 2 * (m1+3) * (m1+2) | _ => maxl l end).
do 2 (prove_rule H).

eexists (fun x => None).
unfold QI.p_smc, QI.p_compatible_QI, QI.p_subterm, QI.p_monotonicity.
repeat split.
(* subterm *)
- intros f l x Hin; assert(H' := maxl_is_max _ _ Hin);
    assert (H'' := maxl_le_suml l); destruct f; simpl; trivial;
  try omega;
  (repeat (destruct l; trivial);
   repeat(destruct Hin as [ H | Hin]; [subst; simpl; try_prove_ineq |]);
   try inversion Hin).
   simpl; nia.
(* monotonic *)
- intros f xs ys Hfor.
  destruct f; qif_monotonic_tac;
  repeat (destruct Hfor; simpl; try qif_monotonic_tac).
- simpl; tauto.
Defined.

Definition qif := proj1_sig qif_proofs.

Proposition qi_is_valid : valid_QI mcs qic qif cs.
Proof.
unfold qif.
destruct qif_proofs as (qif & Hs & Hm & Hc).
repeat split; trivial.
apply qic_bounded.
apply qic_nonzero.
Qed.

(* P-criterion *)
Theorem polytime: forall i s p c f lv d v,
  let t := fapply f lv in
  let pi := cbv_update i s p c t d v in
  cbv_wf pi -> cache_bounded qic qif c ->
  cbv_size pi <= global_bound mcs qif f lv c.
Proof.
intros.
apply P_criterion with (rank:=rank) (cs:=cs) (qic:=qic); auto.
- split; [ apply Expmod_is_wf | trivial ].
- cbv; omega.
- intros f0; destruct f0; cbv; omega.
- apply expmod_is_ppo.
- apply qi_is_valid.
Qed.

(* Specifications *)

(* Conversion functions from/to term values/Coq types. *)
Fixpoint Pos_of_value (v : value) : positive := match v with
| Syntax.c_capply XHC [] => xH
| Syntax.c_capply XOC [v] => xO (Pos_of_value v)
| Syntax.c_capply XIC [v] => xI (Pos_of_value v)
| _ => xH
end.

Fixpoint N_of_value (v : value) : N := match v with
| Syntax.c_capply N0C [] => 0
| Syntax.c_capply NPosC [v] => N.pos (Pos_of_value v)
| _ => 0
end.

Fixpoint value_of_pos (n : positive) : value := match n with
| xH => c_capply XHC []
| xO a => c_capply XOC [value_of_pos a]
| xI a => c_capply XIC [value_of_pos a]
end.

Fixpoint pos_of_value p := match p with
| Syntax.c_capply XHC [] => xH
| Syntax.c_capply XOC [a] => xO (pos_of_value a)
| Syntax.c_capply XIC [a] => xI (pos_of_value a)
| _ => xH
end.

Definition value_of_N (n : N) : Syntax.value EMSyntax.constructor (* value *) :=
  match n with
  | 0%N => c_capply N0C []
  | Npos a => c_capply NposC [value_of_pos a]
  end.

Definition value_of_mask (m : Pos.mask) := match m with
| IsPos a => c_capply IsPosC [value_of_pos a]
| IsNeg => c_capply IsNegC []
| IsNul => c_capply IsNulC []
end.

Definition mask_of_value m := match m with
| Syntax.c_capply IsPosC [a] => IsPos (pos_of_value a)
| Syntax.c_capply IsNegC [] => IsNeg
| Syntax.c_capply IsNulC [] => IsNul
| _ => IsNul
end.

Definition value_of_comp c := match c with
| Eq => c_capply EqC []
| Lt => c_capply LtC []
| Gt => c_capply GtC []
end.

Definition comp_of_value v := match v with
| Syntax.c_capply EqC [] => Eq
| Syntax.c_capply LtC [] => Lt
| Syntax.c_capply GtC [] => Gt
| _ => Eq
end.

Definition value_of_bool b := match b with
| true => c_capply TrueC []
| false => c_capply FalseC []
end.

Definition bool_of_value v := match v with
| Syntax.c_capply TrueC [] => true
| Syntax.c_capply FalseC [] => false
| _ => false
end.

Definition pairN : Type := (N * N).

Definition value_of_pair (x : pairN) := c_capply PairC [value_of_N (fst x); value_of_N (snd x)].

Coercion value_of_N : N >-> Syntax.value.

Coercion value_of_pair : pairN >-> value.

Open Scope N_scope.

Lemma pred_double_correct p : forall t,
evaluates t (value_of_pos p) ->
  evaluates (pred_doubleF (: t :)) (value_of_pos (Pos.pred_double p)).
Proof. induction p; intros; reduce; apply IHp; auto with *. Qed.

Definition pred_double_correct' : ltac:(auto_for_auto pred_double_correct) := pred_double_correct.
Hint Resolve pred_double_correct' : eval.

Lemma succ_double_mask_correct m : forall t,
evaluates t (value_of_mask m) ->
evaluates (succ_double_maskF (: t :))
          (value_of_mask (Pos.succ_double_mask m)).
Proof. induction m; reduce. Qed.

Definition succ_double_mask_correct' : ltac:(auto_for_auto succ_double_mask_correct) := succ_double_mask_correct.
Hint Resolve succ_double_mask_correct' : eval.

Lemma double_mask_correct m : forall t,
evaluates t (value_of_mask m) ->
evaluates (double_maskF (: t :)) (value_of_mask (Pos.double_mask m)).
Proof. induction m; reduce. Qed.

Definition double_mask_correct' : ltac:(auto_for_auto double_mask_correct) := double_mask_correct.
Hint Resolve double_mask_correct' : eval.

Lemma double_pred_mask_correct p : forall t,
evaluates t (value_of_pos p) ->
evaluates (double_pred_maskF (: t :)) (value_of_mask (Pos.double_pred_mask p)).
Proof. induction p; reduce. Qed.

Definition double_pred_mask_correct' : ltac:(auto_for_auto double_pred_mask_correct) := double_pred_mask_correct.
Hint Resolve double_pred_mask_correct' : eval.

Lemma sub_mask_correct q : forall p tp tq,
evaluates tp (value_of_pos p) ->
evaluates tq (value_of_pos q) ->
evaluates (sub_maskF (: tp, tq :))
          (value_of_mask (Pos.sub_mask p q)) /\
evaluates (sub_mask_carryF (: tp, tq :))
          (value_of_mask (Pos.sub_mask_carry p q)).
Proof.
induction q;
intros p tp tq Hp Hq;
destruct p; split; reduce; simpl; fold value_of_pos;
case_eq (Pos.sub_mask p0 q0);
case_eq (Pos.sub_mask_carry p0 q0); intros;
  (econstructor;
  [ reduce; apply IHq; auto with *
  | try rewrite H; try rewrite H0; tauto
  | try reduce; auto with *]).
Qed.

Definition sub_mask_correct' : ltac:(auto_for_auto sub_mask_correct) := sub_mask_correct.
Hint Resolve sub_mask_correct' : eval.

Lemma compare_cont_correct p: forall tp tq q,
evaluates tp (value_of_pos p) ->
evaluates tq (value_of_pos q) ->
evaluates (compare_contEqF (: term_from_value (value_of_pos p),
                              term_from_value (value_of_pos q) :))
          (value_of_comp (Pos.compare_cont Eq p q)) /\
evaluates (compare_contLtF (: term_from_value (value_of_pos p),
                              term_from_value (value_of_pos q) :))
          (value_of_comp (Pos.compare_cont Lt p q)) /\
evaluates (compare_contGtF (: term_from_value (value_of_pos p),
                              term_from_value (value_of_pos q) :))
          (value_of_comp (Pos.compare_cont Gt p q)).
Proof.
induction p; intros tp tq q; destruct q; intros Hp Hq; repeat reduce;
simpl in *;
fold value_of_pos;
eapply IHp; auto with *.
Qed.

Definition compare_cont_correct' : ltac:(auto_for_auto compare_cont_correct) := compare_cont_correct.
Hint Resolve compare_cont_correct' : eval.

Lemma compare_correct p: forall q tp tq,
evaluates tp (value_of_pos p) ->
evaluates tq (value_of_pos q) ->
evaluates (compareF (: tp, tq :)) (value_of_comp (Pos.compare p q)).
Proof.
intros q tp tq Htp Htq; reduce;
eapply (compare_cont_correct p); auto with *.
Qed.

Definition compare_correct' : ltac:(auto_for_auto compare_correct) := compare_correct.
Hint Resolve compare_correct' : eval.

Lemma succ_double_correct t n :
evaluates t (value_of_N n) ->
evaluates (succ_doubleF (: t :)) (value_of_N (N.succ_double n)).
Proof. destruct n; reduce. Qed.

Definition succ_double_correct' : ltac:(auto_for_auto succ_double_correct) := succ_double_correct.
Hint Resolve succ_double_correct' : eval.

Lemma double_correct n : forall t,
evaluates t (value_of_N n) ->
evaluates (doubleF (: t :)) (value_of_N (N.double n)).
Proof. destruct n; reduce. Qed.

Definition double_correct' : ltac:(auto_for_auto double_correct) := double_correct.
Hint Resolve double_correct' : eval.

Lemma sub_correct n m tn tm:
evaluates tn (value_of_N n) ->
evaluates tm (value_of_N m) ->
evaluates (subF (: tn , tm :))
          (value_of_N (N.sub n m)).
Proof.
intros Hn Hm;
destruct n, m; reduce; simpl;
case_eq (Pos.sub_mask p0 p1);
intros;
(econstructor;
[ repeat constructor;
  eapply sub_mask_correct; auto with *
| rewrite H; tauto
| try reduce; auto with eval]).
Qed.

Definition sub_correct' : ltac:(auto_for_auto sub_correct) := sub_correct.
Hint Resolve sub_correct' : eval.

Lemma compare0_correct n: forall m tn tm,
evaluates tn (value_of_N n) ->
evaluates tm (value_of_N m) ->
evaluates (compare0F (: tn, tm :))
          (value_of_comp (N.compare n m)).
Proof. induction n; intro m; intros; destruct m; reduce. Qed.

Definition compare0_correct' : ltac:(auto_for_auto compare0_correct) := compare0_correct.
Hint Resolve compare0_correct' : eval.

Lemma leb_aux_correct : forall tc c,
evaluates tc (value_of_comp c) ->
  evaluates (leb_auxF (: tc :))
             (value_of_bool (match c with Gt => false | _ => true end)).
Proof. intros tc c; destruct c; repeat split; reduce. Qed.

Definition leb_aux_correct' : ltac:(auto_for_auto leb_aux_correct) := leb_aux_correct.
Hint Resolve leb_aux_correct' : eval.

Lemma leb_correct tn tm (n m : N) :
evaluates tn (value_of_N n) ->
evaluates tm (value_of_N m) ->
evaluates (lebF (: tn, tm :)) (value_of_bool (N.leb n m)).
Proof. reduce. Qed.

Definition leb_correct' : ltac:(auto_for_auto leb_correct) := leb_correct.
Hint Resolve leb_correct' : eval.

Lemma cond_correct {A} f tc ta tb c (a b : A) :
evaluates tc (value_of_bool c) ->
evaluates ta (f a) ->
evaluates tb (f b) ->
 evaluates (condF (: tc, ta, tb :))
           (f (if c then a else b)).
Proof. destruct c; reduce. Qed.

Definition cond_correct' A : ltac:(auto_for_auto (@cond_correct A)) := cond_correct.
Hint Resolve cond_correct' : eval.

Lemma mod_succ_double_compat n m :
(if m <=? N.succ_double (n mod m)
 then N.succ_double (n mod m) - m
 else N.succ_double (n mod m)) = N.succ_double n mod m.
Proof.
destruct n as [| n].
- destruct m as [|[m|m|]]; trivial.
- unfold N.modulo.
  case_eq (N.div_eucl (N.pos n) m); intros q r Hqr.
  simpl.
  destruct m as [|m]; trivial; simpl.
  + now simpl in Hqr; inversion Hqr; subst.
  + simpl in Hqr; rewrite Hqr.
    destruct(N.pos m <=? N.succ_double r); trivial.
Qed.

Lemma mod_double_compat n m :
(if m <=? N.double (n mod m)
 then N.double (n mod m) - m
 else N.double (n mod m)) = N.double n mod m.
Proof.
destruct n as [| n].
- destruct m as [|[m|m|]]; trivial.
- unfold N.modulo.
  case_eq (N.div_eucl (N.pos n) m); intros q r Hqr.
  simpl.
  destruct m as [|m]; trivial; simpl.
  + now simpl in Hqr; inversion Hqr; subst.
  + simpl in Hqr; rewrite Hqr.
    destruct(N.pos m <=? N.double r); trivial.
Qed.

Lemma mod_aux_correct n m tn tm:
evaluates tn (value_of_pos n) ->
evaluates tm (value_of_N m) ->
evaluates (mod_auxF (: tn, tm :)) (value_of_N (N.modulo (N.pos n) m)).
Proof.
revert tn tm.
induction n; intros tn tm Hn Hm.
- reduce; evar (v1: N); evar (v2: N).
  replace (N.pos n~1 mod m) with
          (if m <=? N.succ_double (N.pos n mod m) then v1 else v2).
  apply cond_correct.
  + apply leb_correct; simpl; auto with *.
    apply succ_double_correct; auto with *.
  + apply sub_correct.
    apply succ_double_correct.
    apply IHn; auto with *.
    simpl; auto with *.
  + apply succ_double_correct.
    apply IHn; auto with *.
  + subst v1 v2.
    apply mod_succ_double_compat.
- reduce; evar (v1: N); evar (v2: N).
  replace (N.pos n~0 mod m) with
          (if m <=? N.double (N.pos n mod m) then v1 else v2).
  apply cond_correct.
  + apply leb_correct; simpl; auto with *.
    apply double_correct; auto with *.
  + apply sub_correct.
    apply double_correct.
    apply IHn; auto with *.
    simpl; auto with *.
  + apply double_correct.
    apply IHn; auto with *.
  + subst v1 v2.
    apply mod_double_compat.
- destruct m as [| [ m | m |]]; simpl; reduce.
Qed.

Definition mod_aux_correct' : ltac:(auto_for_auto mod_aux_correct) := mod_aux_correct.
Hint Resolve mod_aux_correct' : eval.

Lemma mod_0 n : n mod 0 = n.
Proof.
destruct n; trivial.
Qed.

Lemma mod_correct n m tn tm:
evaluates tn (value_of_N n) ->
evaluates tm (value_of_N m) ->
evaluates (modF (: tn, tm :)) (value_of_N (N.modulo n m)).
Proof.
destruct n; reduce.
Qed.

Definition mod_correct' : ltac:(auto_for_auto mod_correct) := mod_correct.
Hint Resolve mod_correct' : eval.

Lemma succ_correct p: forall t,
evaluates t (value_of_pos p) ->
evaluates (succF (: t :)) (value_of_pos (Pos.succ p)).
Proof. induction p; intros; reduce; apply IHp; auto with *. Qed.

Lemma add_correct p: forall q tp tq,
evaluates tp (value_of_pos p) ->
evaluates tq (value_of_pos q) ->
evaluates (addF (: tp, tq :)) (value_of_pos (Pos.add p q)) /\
evaluates (add_carryF (: tp, tq :)) (value_of_pos (Pos.add_carry p q)).
Proof.
induction p; intros q tp tq Hp Hq; split; destruct q; reduce;
try (apply IHp || apply succ_correct); auto with *.
Qed.

Lemma add0_correct n m: forall tn tm,
evaluates tn (value_of_N n) ->
evaluates tm (value_of_N m) ->
evaluates (add0F (: tn, tm :)) (value_of_N (N.add n m)).
Proof.
destruct n; intros; [ reduce |];
destruct m; [ reduce | reduce; apply add_correct; auto with * ].
Qed.

Inductive larger_bound : positive -> positive -> Type :=
  | larger_1  : forall b, larger_bound xH b
  | larger_xI : forall x b, larger_bound x b -> larger_bound (xI x) (xO b)
  | larger_xO : forall x b, larger_bound x b -> larger_bound (xO x) (xO b).

Lemma larger_bound_xO p b:
 larger_bound p b -> larger_bound p b~0.
Proof.
intro H; induction H; constructor; assumption.
Qed.

Lemma mul_mod_aux_correct p1 p2 m: forall n tp1 tp2 tn tm,
m <> 0 ->
larger_bound p1 p2 ->
evaluates tp1 (value_of_pos p1) ->
evaluates tp2 (value_of_pos p2) ->
evaluates tn (value_of_N n) ->
evaluates tm (value_of_N m) ->
evaluates (mul_mod_auxF (: tp1, tn, tm, tp2 :))
          ((N.pos p1 * n) mod m).
Proof.
revert p2.
induction p1 as [ p | p |]; intros p2 n tp1 tp2 tn tm Hpos Hb H1 H2 Hn Hm;
inversion Hb; subst; reduce.
- replace (N.pos p~1 * n) with (n + N.double (N.pos p * n)) by (now destruct n).
  rewrite <- N.add_mod_idemp_r; trivial.
  rewrite N.double_spec.
  rewrite <- N.mul_mod_idemp_r; trivial.
  rewrite <- N.double_spec.
  rewrite N.add_mod_idemp_r; trivial.
  apply mod_correct; auto with *.
  apply add0_correct; auto with *.
  apply double_correct; auto with *.
  apply IHp with (p2 := b); auto with *.
- replace (N.pos p~0 * n) with (N.double (N.pos p * n)) by (now destruct n).
  rewrite N.double_spec.
  rewrite <- N.mul_mod_idemp_r; trivial.
  rewrite <- N.double_spec.
  apply mod_correct; auto with *.
  apply double_correct; auto with *.
  apply IHp with (p2 := b); auto with *.
- apply mod_correct.
  + destruct n; auto with eval.
  + auto with *.
Qed.

Definition N_larger_bound n b := match n with
| 0 => larger_bound xH b
| Npos p0 => larger_bound p0 b
end.

Fixpoint lower_bound p0 := match p0 with
| xH => xH
| xO p0 => xO (lower_bound p0)
| xI p0 => xO (lower_bound p0)
end.

Lemma lower_bound_bound p0 : larger_bound p0 (lower_bound p0).
Proof.
induction p0; now constructor.
Qed.

Lemma lower_bound_pow2 k : (lower_bound (2^ k) = 2^k)%positive.
Proof.
induction k using Pos.peano_ind.
- simpl; trivial.
- simpl.
  rewrite Pos.pow_succ_r.
  simpl; now f_equal.
Qed.

Lemma lower_bound_div_bound (p0 b : positive) :
larger_bound p0 b -> {k | (b = k * lower_bound p0)%positive}.
Proof.
revert b; induction p0; intros b Hb; inversion Hb; subst.
- destruct (IHp0 b0 H0) as (k & Hk).
  exists k; simpl; lia.
- destruct (IHp0 b0 H0) as (k & Hk).
  exists k; simpl; lia.
- exists b; simpl; lia.
Qed.

Lemma lower_bound_le p0 p1 :
(p0 <= p1 -> {k | lower_bound p1 = k * lower_bound p0})%positive.
Proof.
revert p1.
induction p0; intros p1 Hle.
- destruct p1 as [p1|p1|].
  + simpl in Hle.
    assert(Hle' : (p0 <= p1)%positive) by lia.
    apply IHp0 in Hle'.
    destruct Hle' as [k Hk].
    exists k;simpl;lia.
  + simpl in Hle.
    assert(Hle' : (p0 <= p1)%positive) by lia.
    apply IHp0 in Hle'.
    destruct Hle' as [k Hk].
    exists k;simpl;lia.
  + contradict Hle; lia.
- destruct p1 as [p1|p1|].
  + simpl in Hle.
    assert(Hle' : (p0 <= p1)%positive) by lia.
    apply IHp0 in Hle'.
    destruct Hle' as [k Hk].
    exists k;simpl;lia.
  + simpl in Hle.
    assert(Hle' : (p0 <= p1)%positive) by lia.
    apply IHp0 in Hle'.
    destruct Hle' as [k Hk].
    exists k;simpl;lia.
  + contradict Hle; lia.
- exists (lower_bound p1); simpl; lia.
Qed.

Lemma larger_bound_spec p0 k:
  larger_bound p0 (k * lower_bound p0).
Proof.
induction p0.
- simpl; rewrite Pos.mul_xO_r; now constructor.
- simpl; rewrite Pos.mul_xO_r; now constructor.
- constructor.
Qed.

Lemma N_larger_bound_le n n' b :
 n' <= n ->
 N_larger_bound n b ->
 N_larger_bound n' b.
Proof.
intros Hle Hb.
destruct n' as [| n'].
- simpl; constructor.
- destruct n as [| n]; [ now destruct Hle |].
  simpl in *.
  destruct (lower_bound_div_bound n b Hb) as (k & Hk).
  apply lower_bound_le in Hle.
  destruct Hle as (k' & Hk').
  rewrite Hk' in Hk.
  rewrite Hk.
  replace (k * (k' * lower_bound n'))%positive
    with (k * k' * lower_bound n')%positive by lia.
  apply larger_bound_spec.
Qed.

Lemma N_larger_bound_mod n m b :
 m <> 0 ->
 N_larger_bound m b ->
 N_larger_bound (n mod m) b.
Proof.
intro H; now apply N_larger_bound_le, N.lt_le_incl, N.mod_lt.
Qed.

Hint Resolve N_larger_bound_mod : eval.

Lemma mul_mod_correct n n' m b: forall tn tn' tm tb,
m <> 0 ->
N_larger_bound n b ->
evaluates tn (value_of_N n) ->
evaluates tn' (value_of_N n') ->
evaluates tm (value_of_N m) ->
evaluates tb (value_of_pos b) ->
evaluates (mul_modF (: tn, tn', tm, tb:))
          ((n * n') mod m).
Proof.
intros; destruct n; reduce.
apply mul_mod_aux_correct with (p2 := b); auto with eval.
Qed.

Lemma exp_mod_aux_correct y: forall x m tx ty tm b tb,
m <> 0 ->
N_larger_bound m b ->
evaluates tx (value_of_N x) ->
evaluates ty (value_of_pos y) ->
evaluates tm (value_of_N m) ->
evaluates tb (value_of_pos b) ->
evaluates (exp_mod_auxF (: tx, ty, tm, tb :))
          ( x ^ (Npos y) mod m).
Proof.
induction y as [ y | y | ]; intros x m tx ty tm b tb Hpos Hlarger Hx Hy Hm Hb.
- change (Npos y~1) with (N.succ (N.pos y~0)).
  rewrite N.pow_succ_r; [ | lia].
  change (N.pos y~0) with (2 * (N.pos y)).
  rewrite N.pow_mul_r, <- N.mul_mod_idemp_r; trivial.
  rewrite <- N.mod_mod; trivial.
  rewrite <- N.mul_mod_idemp_l; trivial.
  rewrite N.mod_mod; trivial.
  reduce.
  apply mul_mod_correct with b; auto with *.
  rewrite N.pow_2_r.
  rewrite N.pow_mul_l, N.mul_mod; trivial.
  apply mul_mod_correct with b; auto with *;
  apply IHy with b; auto with *.
- change (N.pos y~0) with (2 * (N.pos y)).
  rewrite N.pow_mul_r, N.pow_2_r, N.pow_mul_l, N.mul_mod; trivial.
  reduce.
  apply mul_mod_correct with b; auto with *;
  apply IHy with b; auto with *.
- reduce.
  apply mod_correct; simpl; auto with *.
  destruct x; auto with *.
  rewrite Pos.pow_1_r; auto with *.
Qed.

Lemma bound_correct_pos x tx:
evaluates tx (value_of_pos x) ->
evaluates (boundF (: tx :)) (value_of_pos (2^(Pos.size x))).
Proof.
revert tx.
induction x; intros; reduce; simpl;
rewrite Pos.pow_succ_r; reduce; apply IHx; auto with *.
Qed.

Lemma exp_mod_correct x y m tx ty tm:
m <> 0 ->
evaluates tx (value_of_N x) ->
evaluates ty (value_of_N y) ->
evaluates tm (value_of_N m) ->
evaluates (exp_modF (: tx, ty, tm :))
          ( x ^ y mod m).
Proof.
intros.
destruct y as [ | y].
- reduce.
  apply mod_correct; [ reduce | auto with *].
- reduce.
  destruct m as [|m].
  + apply exp_mod_aux_correct with (b := xH); tauto.
  + apply exp_mod_aux_correct with (b := (2^(Pos.size m))%positive); auto with *.
    * assert (m <= 2^ Pos.size m)%positive by
      (apply Pos.lt_le_incl, Pos.size_gt).
      apply N_larger_bound_le with (n := N.pos (2 ^ Pos.size m)); trivial.
      simpl; rewrite <- lower_bound_pow2 at 2.
      apply lower_bound_bound.
    * reduce; apply bound_correct_pos; auto with *.
Qed.

author: UCSD-PL


text:
(*

  Copyright 2016 Luxembourg University
  Copyright 2017 Luxembourg University

  This file is part of Velisarios.

  Velisarios is free software: you can redistribute it and/or modify
  it under the terms of the GNU General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
  (at your option) any later version.

  Velisarios is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  GNU General Public License for more details.

  You should have received a copy of the GNU General Public License
  along with Velisarios.  If not, see <http://www.gnu.org/licenses/>.

  Authors: Vincent Rahli
           Ivana Vukotic

*)

Require Export PBFTprops3.
Require Export PBFTwell_formed_log.

Section PBFTpre_prepare_in_log_preserves.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { pbft_context : PBFTcontext      }.
  Context { pbft_auth    : PBFTauth         }.
  Context { pbft_keys    : PBFTinitial_keys }.
  Context { pbft_hash    : PBFThash         }.

  Lemma add_new_commit2log_preserves_pre_prepare_in_log :
    forall d p c L1 L2 i,
      add_new_commit2log L1 c = (i, L2)
      -> pre_prepare_in_log p d L2 = pre_prepare_in_log p d L1.
  Proof.
    induction L1; introv h; simpl in *; tcsp; smash_pbft.

    { pbft_simplifier; simpl in *; pbft_dest_all w. }

    - match goal with
      | [H : add_commit2entry _ _ = _ |- _ ] =>
        apply add_commit2entry_preserves_log_entry_pre_prepare_info in H
      end.
      allrw. auto.

    - match goal with
      | [H : add_commit2entry _ _ = _ |- _ ] =>
        apply add_commit2entry_preserves_log_entry_request_data in H
      end.
      allrw similar_entry_and_pre_prepare_true_iff.
      allrw similar_entry_and_pre_prepare_false_iff.
      rewrite <- Heqx1 in Heqx2. tcsp.

    - match goal with
      | [H : add_commit2entry _ _ = _ |- _ ] =>
        apply add_commit2entry_preserves_log_entry_request_data in H
      end.
      allrw similar_entry_and_pre_prepare_true_iff.
      allrw similar_entry_and_pre_prepare_false_iff.
      rewrite <- Heqx1 in Heqx2. tcsp.
  Qed.

  Lemma entry_of_pre_prepare_in_log :
    forall d p L,
      pre_prepare_in_log p d L = true
      -> exists entry,
        In entry L
        /\ log_entry_request_data entry = pre_prepare2request_data p d.
  Proof.
    induction L; introv h; simpl in *; tcsp.
    pbft_dest_all x.

    - exists a; dands; tcsp.
      allrw similar_entry_and_pre_prepare_true_iff; auto.

    - apply IHL in h; exrepnd; exists entry; auto.
  Qed.

  Lemma clear_log_checkpoint_preserves_pre_prepare_in_log :
    forall d p L sn,
      well_formed_log L
      -> pre_prepare_in_log p d (clear_log_checkpoint L sn) = true
      -> pre_prepare_in_log p d L = true.
  Proof.
    induction L; simpl in *; introv wf h; tcsp.
    pbft_dest_all x.

    - assert False; tcsp.

      inversion wf as [|? ? imp wfL]; subst; clear wf.
      apply IHL in h; auto.

      allrw similar_entry_and_pre_prepare_true_iff.

      match goal with
      | [ H : pre_prepare_in_log _ _ _ = _ |- _ ] => apply entry_of_pre_prepare_in_log in H
      end.
      exrepnd.
      pose proof (imp entry) as q; autodimp q hyp; apply q; auto.
      allrw; auto.

    - inversion wf as [|? ? imp wfL]; subst; clear wf.
      apply IHL in h; auto.

    - inversion wf as [|? ? imp wfL]; subst; clear wf.
      apply IHL in h; auto.
  Qed.

  Lemma check_stable_preserves_pre_prepare_in_log :
    forall d slf state entryop state' p,
      well_formed_log (log state)
      -> check_stable slf state entryop = Some state'
      -> pre_prepare_in_log p d (log state') = true
      -> pre_prepare_in_log p d (log state) = true.
  Proof.
    introv wf h q.
    unfold check_stable in h.
    pbft_dest_all x;[].
    apply clear_log_checkpoint_preserves_pre_prepare_in_log in q; auto.
  Qed.

  Lemma change_entry_add_replies2entry_preserves_pre_prepare_in_log :
    forall d prep sn entry L reps,
      pre_prepare_in_log
        d prep
        (change_entry L (add_replies2entry entry reps)) = true
      -> find_entry L sn = Some entry
      -> pre_prepare_in_log d prep L = true.
  Proof.
    induction L; introv h fe; simpl in *; tcsp.
    smash_pbft;[| | | |];
      try (complete (applydup entry2seq_if_find_entry in fe as eqsn;
                     match goal with
                     | [ H : similar_entry _ _ = _ |- _ ] => apply entry2seq_if_similar_entry in H
                     end;
                     match goal with
                     | [ H : _ <> _ |- _ ] => destruct H; allrw; auto
                     end));[|].

    - repnd.
      allrw similar_entry_and_pre_prepare_false_iff.

      match goal with
      | [ H : _ <> _ |- _ ] => destruct H; allrw; auto
      end.

      unfold rep_toks_matches_logEntryPrePrepareInfo in *.
      destruct (log_entry_pre_prepare_info entry);[|]; simpl in *; tcsp.
      smash_pbft.
      allrw similar_entry_and_pre_prepare_true_iff.

      rewrite log_entry_request_data_add_replies2entry in Heqx0.
      auto.

    - allrw similar_entry_and_pre_prepare_false_iff.
      rewrite log_entry_request_data_add_replies2entry in Heqx0.
      unfold rep_toks_matches_logEntryPrePrepareInfo in *.
      destruct (log_entry_pre_prepare_info entry);simpl in *;
        allrw similar_entry_and_pre_prepare_true_iff; tcsp.
  Qed.

  Lemma change_log_entry_add_replies2entry_preserves_pre_prepare_in_log :
    forall d prep sn entry state reps,
      pre_prepare_in_log
        d prep
        (log
           (change_log_entry
              state
              (add_replies2entry entry reps))) = true
      -> find_entry (log state) sn = Some entry
      -> pre_prepare_in_log d prep (log state) = true.
  Proof.
    introv h fe.
    destruct state; simpl in *.
    eapply change_entry_add_replies2entry_preserves_pre_prepare_in_log in h;[|eauto].
    auto.
  Qed.

  Lemma find_and_execute_requests_preserves_pre_prepare_in_log :
    forall d msg i prep st p,
      find_and_execute_requests i (current_view p) (local_keys p) p = (msg, st)
      -> pre_prepare_in_log d prep (log st) = true
      -> pre_prepare_in_log d prep (log p) = true.
  Proof.
    introv H1 H2.

    unfold find_and_execute_requests in *.
    pbft_dest_all x;[].
    rename x1 into st.
    unfold execute_requests in *.
    destruct (ready p); simpl in *;[ inversion Heqx; allrw; tcsp |].

    pbft_dest_all y.

    match goal with
    | [ H : context[reply2requests] |- _ ] => hide_hyp H
    end.

    match goal with
    | [ H : check_broadcast_checkpoint _ _ _ _ _ = _ |- _ ] =>
      apply check_broadcast_checkpoint_preserves_log in H
    end.

    match goal with
    | [ H1 : pre_prepare_in_log _ _ (log ?s) = _, H2 : _ = log ?s |- _ ] =>
      rewrite <- H2 in H1; clear H2
    end.

    pose proof (change_log_entry_add_replies2entry_preserves_pre_prepare_in_log
                  d prep (next_to_execute p) y p y3) as xx.
    apply xx in H2; auto.
  Qed.
  Hint Resolve find_and_execute_requests_preserves_pre_prepare_in_log : pbft.

  Lemma check_send_replies_preserves_pre_prepare_in_log :
    forall d prep slf view keys entryop state sn msgs state',
      check_send_replies slf view keys entryop state sn = (msgs, state')
      -> pre_prepare_in_log d prep (log state') = true
      -> pre_prepare_in_log d prep (log state) = true.
  Proof.
    introv chk pil.
    unfold check_send_replies in chk.
    destruct entryop; smash_pbft.
    destruct g; smash_pbft.
  Qed.
  Hint Resolve check_send_replies_preserves_pre_prepare_in_log : pbft.

  Lemma add_new_prepare2log_preserves_pre_prepare_in_log :
    forall i d gi Fc prep new_prep L new_log,
      add_new_prepare2log i L new_prep Fc = (gi, new_log)
      -> pre_prepare_in_log d prep new_log = true
      -> pre_prepare_in_log d prep L = true.
  Proof.
    induction L; introv IH1 IH2; simpl in *; smash_pbft;
    try (complete(allrw is_prepare_for_entry_true_iff;
                  allrw is_prepare_for_entry_false_iff;
                  destruct x;[]; simpl in *;
                  unfold add_prepare2entry in *;
                  destruct a;[]; simpl in *;
                  smash_pbft)).

    { pbft_simplifier; simpl in *; pbft_dest_all w. }
  Qed.

  Lemma add_new_pre_prepare_and_prepare2log_preserves_pre_prepare_in_log :
    forall i L pp d Fp Fc giop K prep d',
      add_new_pre_prepare_and_prepare2log i L pp d Fp Fc = (giop, K)
      -> pre_prepare_in_log prep d' K = true
      -> pre_prepare_in_log prep d' L = true
         \/
         (
           prep = pp
           /\ d = d'
           /\ pre_prepare_in_log prep d' L = false
         ).
  Proof.
    induction L; introv h q; simpl in *; smash_pbft.

    {
      simpl in *; smash_pbft.

      destruct pp, prep.
      destruct b, b0.
      simpl in *.
      smash_pbft.
      unfold eq_request_data in *; simpl in *; smash_pbft; ginv.
      match goal with
      | [ H : matching_requests _ _ = _ |- _ ] =>
        apply matching_requests_true_iff in H
      end.
      allrw map_map; simpl.
      allrw map_id; subst; tcsp.
    }

    {
      exrepnd.
      destruct x; simpl in *.
      unfold fill_out_pp_info_with_prepare in *.
      destruct a; simpl in *.
      destruct log_entry_pre_prepare_info; simpl in *; ginv; simpl in *; tcsp.
      smash_pbft;[].

      unfold eq_request_data in *.
      pbft_dest_all y;[].

      allrw auth_matches_logEntryPrePrepareInfo_pre_prepare2pp_info_true_iff.
      allrw requests_matches_logEntryPrePrepareInfo_true_iff.

      exrepnd.

      unfold add_prepare_if_not_enough in *.
      smash_pbft;[|];
        try (complete (right; destruct pp, prep; destruct b, b0;
                       simpl in *; subst; GC; ginv)).
    }

    {
      allrw similar_entry_and_pre_prepare_true_iff.
      allrw similar_entry_and_pre_prepare_false_iff.

      match goal with
      | [ H : fill_out_pp_info_with_prepare _ _ _ _ _ = _ |- _ ] =>
        applydup fill_out_pp_info_with_prepare_preserves_request_data in H as z;
          symmetry in z
      end.

      rewrite <-  Heqx1 in Heqx2. tcsp.
    }

    {

      match goal with
      | [ H : fill_out_pp_info_with_prepare _ _ _ _ _ = _ |- _ ] =>
        applydup fill_out_pp_info_with_prepare_preserves_request_data in H as z;
          symmetry in z;
          eapply  eq_request_data_preserves_similar_entry_and_pre_prepare in z;[|eauto];pbft_simplifier
      end.
    }
  Qed.

  Lemma rep_toks_matches_logEntryPrePrepareInfo_true_iff :
    forall rt i nfo,
      rep_toks_matches_logEntryPrePrepareInfo rt i nfo = true
      <->
      exists auth reqs,
        nfo = pp_info_pre_prep auth reqs
        /\ rt = MkRepToks i auth.
  Proof.
    introv; unfold rep_toks_matches_logEntryPrePrepareInfo; split;
      intro h; destruct nfo; exrepnd; subst; smash_pbft; ginv; eauto.
  Qed.

  Lemma auth_matches_logEntryPrePrepareInfo_true_iff :
    forall a nfo,
      auth_matches_logEntryPrePrepareInfo a nfo = true
      <->
      exists reqs,
        nfo = pp_info_pre_prep a reqs.
  Proof.
    introv; unfold auth_matches_logEntryPrePrepareInfo; split;
      intro h; destruct nfo; exrepnd; subst; smash_pbft; ginv; eauto.
  Qed.

  Lemma pre_prepare_in_log_add_new_prepare2log :
    forall pp d npp nd L,
      pre_prepare_in_log pp d (add_new_pre_prepare2log npp nd L) = true
      -> pre_prepare_in_log pp d L = true
         \/
         (pp = npp /\ d = nd /\ pre_prepare_in_log pp d L = false).
  Proof.
    induction L; introv h; simpl in *; smash_pbft;[|].

    - right.
      unfold eq_request_data in *; smash_pbft.
      repnd.
      allrw auth_matches_logEntryPrePrepareInfo_pre_prepare2pp_info_true_iff.
      allrw requests_matches_logEntryPrePrepareInfo_true_iff; repnd.
      autorewrite with pbft in *; dands; eauto 3 with pbft.

    - clear IHL.
      repnd; GC.
      allrw auth_matches_logEntryPrePrepareInfo_pre_prepare2pp_info_true_iff.
      allrw requests_matches_logEntryPrePrepareInfo_true_iff; repnd.
      allrw similar_entry_and_pre_prepare_true_iff.

      match goal with
      | [ H1 : log_entry_request_data ?x = _, H2 : log_entry_request_data ?x = _ |- _ ] =>
        rewrite H1 in H2
      end.

      smash_pbft.

      match goal with
      | [ |- context[auth_matches_logEntryPrePrepareInfo ?x ?y] ] =>
        remember (auth_matches_logEntryPrePrepareInfo x y) as b
      end.
      symmetry in Heqb; destruct b; tcsp;
        [|right; dands; eauto 3 with pbft].

      rewrite auth_matches_logEntryPrePrepareInfo_true_iff in Heqb; exrepnd.
      rewrite Heqb0 in *; simpl in *.

      remember (matching_requests (pre_prepare2requests pp) (map fst reqs)) as w.
      symmetry in Heqw; destruct w; tcsp.
  Qed.

  Lemma pre_prepare_in_log_add_new_pre_prepare2log_false_implies :
    forall pp d pp' d' L,
      pre_prepare_in_log pp d (add_new_pre_prepare2log pp' d' L) = false
      -> pre_prepare_in_log pp d L = false.
  Proof.
    induction L; introv h; simpl in *; smash_pbft.
    repndors; smash_pbft; tcsp; GC;
      destruct a, log_entry_pre_prepare_info; simpl in *; tcsp.
  Qed.
  Hint Resolve pre_prepare_in_log_add_new_pre_prepare2log_false_implies : pbft.

  Lemma pre_prepare_in_log_log_pre_prepares_implies :
    forall pp d P L lwm,
      pre_prepare_in_log pp d (log_pre_prepares L lwm P) = true
      -> pre_prepare_in_log pp d L = true
         \/
         (
           In (pp,d) P
           /\ pre_prepare_in_log pp d L = false
           /\ lwm < pre_prepare2seq pp
         ).
  Proof.
    induction P; introv h; simpl in *; tcsp.
    repnd; simpl in *; smash_pbft; apply IHP in h; repndors; repnd; tcsp;[|].

    - apply pre_prepare_in_log_add_new_prepare2log in h; repndors; repnd; subst; tcsp.

    - apply pre_prepare_in_log_add_new_pre_prepare2log_false_implies in h1; tcsp.
  Qed.

  Lemma add_prepare_to_log_from_new_view_pre_prepare_preserves_pre_prepare_in_log :
    forall d' slf prep pp d state state' msgs,
      add_prepare_to_log_from_new_view_pre_prepare slf state (pp,d) = (state', msgs)
      -> pre_prepare_in_log prep d' (log state') = true
      -> pre_prepare_in_log prep d' (log state) = true
         \/
         (
           prep = pp
           /\ d = d'
           /\ low_water_mark state < pre_prepare2seq pp
           /\ pre_prepare_in_log prep d' (log state) = false
         ).
  Proof.
    introv h q.
    unfold add_prepare_to_log_from_new_view_pre_prepare in h; smash_pbft.

    match goal with
    | [ H : check_send_replies _ _ _ _ _ _ = _ |- _ ] =>
      apply check_send_replies_preserves_log in H; simpl in *; subst
    end.

    match goal with
    | [ H : add_new_pre_prepare_and_prepare2log _ _ _ _ _ _ = _ |- _ ] =>
      eapply add_new_pre_prepare_and_prepare2log_preserves_pre_prepare_in_log in H;[|eauto]
    end.

    repndors; tcsp.
  Qed.

  Lemma add_prepares_to_log_from_new_view_pre_prepares_preserves_pre_prepare_in_log :
    forall d' slf prep pps state state' msgs,
      add_prepares_to_log_from_new_view_pre_prepares slf state pps = (state', msgs)
      -> pre_prepare_in_log prep d' (log state') = true
      -> pre_prepare_in_log prep d' (log state) = true
         \/
         exists pp d,
           In (pp,d) pps
           /\ prep = pp
           /\ d = d'
           /\ low_water_mark state < pre_prepare2seq pp
           /\ pre_prepare_in_log prep d' (log state) = false.
  Proof.
    induction pps; introv h q; simpl in *; smash_pbft; repnd.

    match goal with
    | [ H : add_prepares_to_log_from_new_view_pre_prepares _ _ _ = _ |- _ ] =>
      applydup IHpps in H;auto;[]
    end.
    repndors; tcsp;[|].

    {
      match goal with
      | [ H : add_prepare_to_log_from_new_view_pre_prepare _ _ _ = _ |- _ ] =>
        eapply add_prepare_to_log_from_new_view_pre_prepare_preserves_pre_prepare_in_log in H;[|eauto]
      end.

      repndors; repnd; tcsp; subst.
      right.
      exists a0 d'; dands; auto.
    }

    {
      exrepnd; repnd; subst; tcsp.

      rename_hyp_with add_prepare_to_log_from_new_view_pre_prepare add.
      applydup add_prepare_to_log_from_new_view_pre_prepare_preserves_cp_state in add.
      apply eq_low_water_marks_if_eq_cp_states in add0.
      rewrite <- add0.

      remember (pre_prepare_in_log pp d' (log state)) as b.
      symmetry in Heqb; destruct b; tcsp.
      right.
      exists pp d'; dands; auto.
    }
  Qed.

  (*Lemma update_state_new_view_preserves_pre_prepare_in_log :
    forall i st nv st' msgs pp d,
      update_state_new_view i st nv = (st', msgs)
      -> pre_prepare_in_log pp d (log st) = true
      -> pre_prepare_in_log pp d (log st') = true.
  Proof.
    introv u prep.
    unfold update_state_new_view in u; smash_pbft.
    rename_hyp_with log_checkpoint_cert_from_new_view chk.
    apply log_checkpoint_cert_from_new_view_preserves_log in chk.
    rewrite <- chk.

    SearchAbout clear_log_checkpoint.
XXXXXXXX
    Check clear_log_checkpoint_preserves_pre_prepare_in_log.
    eapply clear_log_checkpoint_preserves_pre_prepare_in_log; eauto.
    allrw <- ; auto.
    apply update_state_new_view_preserves_log in u; allrw <-; auto.
  Qed.
  Hint Resolve update_state_new_view_preserves_pre_prepare_in_log : pbft.*)

  Lemma pre_prepare_in_log_log_pre_prepares_false :
    forall pp d P L lwm,
      pre_prepare_in_log pp d (log_pre_prepares L lwm P) = false
      -> pre_prepare_in_log pp d L = false.
  Proof.
    induction P; introv h; simpl in *; auto.
    repnd; simpl in *; smash_pbft.
  Qed.
  Hint Resolve pre_prepare_in_log_log_pre_prepares_false : pbft.

  Lemma log_checkpoint_cert_from_new_view_preserves_pre_prepare_in_log :
    forall i st v x1 C S st' x3 pp d,
      log_checkpoint_cert_from_new_view i st v x1 C S = (st', x3)
      -> pre_prepare_in_log pp d (log st') = pre_prepare_in_log pp d (log st).
  Proof.
    introv h.
    unfold log_checkpoint_cert_from_new_view in h; smash_pbft.
  Qed.
  Hint Resolve log_checkpoint_cert_from_new_view_preserves_pre_prepare_in_log : pbft.

  (*Lemma log_update_low_water_mark :
    forall s n, log (update_low_water_mark s n) = log s.
  Proof.
    tcsp.
  Qed.
  Hint Rewrite log_update_low_water_mark : pbft.*)

  Lemma update_state_new_view_preserves_pre_prepare_in_log :
    forall i st nv st' msgs pp d,
      well_formed_log (log st)
      -> update_state_new_view i st nv = (st', msgs)
      -> pre_prepare_in_log pp d (log st') = true
      -> pre_prepare_in_log pp d (log st) = true.
  Proof.
    introv wf upd prep; unfold update_state_new_view in upd; smash_pbft.
    rename_hyp_with log_checkpoint_cert_from_new_view chk.
    apply log_checkpoint_cert_from_new_view_preserves_log in chk.
    rewrite chk.
    eapply clear_log_checkpoint_preserves_pre_prepare_in_log; eauto.
    allrw <- ; auto.
  Qed.
  Hint Resolve update_state_new_view_preserves_pre_prepare_in_log : pbft.

  Lemma pre_prepare_in_log_check_one_stable :
    forall pp d i s l,
      well_formed_log (log s)
      -> pre_prepare_in_log pp d (log (check_one_stable i s l)) = true
      -> pre_prepare_in_log pp d (log s) = true.
  Proof.
    induction l; introv wf prep; simpl in *; smash_pbft.
    rename_hyp_with check_stable check.
    eapply check_stable_preserves_pre_prepare_in_log; eauto.
  Qed.
  Hint Resolve pre_prepare_in_log_check_one_stable : pbft.

End PBFTpre_prepare_in_log_preserves.

Hint Resolve check_send_replies_preserves_pre_prepare_in_log : pbft.
Hint Resolve pre_prepare_in_log_log_pre_prepares_false : pbft.
Hint Resolve log_checkpoint_cert_from_new_view_preserves_pre_prepare_in_log : pbft.
Hint Resolve update_state_new_view_preserves_pre_prepare_in_log : pbft.
Hint Resolve pre_prepare_in_log_add_new_pre_prepare2log_false_implies : pbft.
Hint Resolve pre_prepare_in_log_check_one_stable : pbft.
Hint Resolve find_and_execute_requests_preserves_pre_prepare_in_log : pbft.
(*Hint Rewrite @log_update_low_water_mark : pbft.*)

author: vrahli

repo: Velisarios

save_path: github-repos/coq/vrahli-Velisarios


text:
(*************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(*************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(*************************************************************)

Require Import List Arith Lia.

From Undecidability.Shared.Libs.DLW
  Require Import utils list_bool pos vec
                 subcode sss compiler_correction.

From Undecidability.StackMachines.BSM
  Require Import bsm_defs.

From Undecidability.MinskyMachines.MM
  Require Import mm_defs mm_utils.

Set Implicit Arguments.

Set Default Proof Using "Type".

(* ** BSM recues to MM *)

Tactic Notation "rew" "length" := autorewrite with length_db.

Local Notation "e #> x" := (vec_pos e x).
Local Notation "e [ v / x ]" := (vec_change e x v).

Local Notation "I '/BSM/' s -1> t" := (bsm_sss I s t) (at level 70, no associativity).
Local Notation "P '/BSM/' s -+> t" := (sss_progress (@bsm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/BSM/' s ->> t" := (sss_compute (@bsm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/BSM/' s ~~> t" := (sss_output (@bsm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/BSM/' s ↓" := (sss_terminates (@bsm_sss _) P s)(at level 70, no associativity).

Local Notation "P '/MM/' s -+> t" := (sss_progress (@mm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/MM/' s ->> t" := (sss_compute (@mm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/MM/' s '~~>' t" := (sss_output (@mm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/MM/' s ↓" := (sss_terminates (@mm_sss _) P s)(at level 70, no associativity).

Section simulator.

  Ltac dest x y := destruct (pos_eq_dec x y) as [ | ]; [ subst x | ]; rew vec.

  Variables (m : nat).

  (* each stack of the BSM corresponds to a (unique) register in the MM
      and there are extra registers: tmp1, tmp2 which must have value 0 at start
      they might change value during a simulated BSM instruction but when
      the instruction is finished, their values are back to 0

      This is expressed in the below bsm_state_enc invariant
  *)

  Let n := 2+m.
  Local Definition tmp1 : pos n := pos0.
  Local Definition tmp2 : pos n := pos1.
  Local Definition reg p: pos n := pos_nxt (pos_nxt p).

  Local Lemma Hv12 : tmp1 <> tmp2.             Proof. discriminate. Qed.
  Local Lemma Hvr1 : forall p, reg p <> tmp1.  Proof. discriminate. Qed.
  Local Lemma Hvr2 : forall p, reg p <> tmp2.  Proof. discriminate. Qed.

  Let Hreg : forall p q, reg p = reg q -> p = q.
  Proof. intros; do 2 apply pos_nxt_inj; apply H. Qed.

  Definition bsm_state_enc (v : vec (list bool) m) w :=
            w#>tmp1 = 0
         /\ w#>tmp2 = 0
         /\ forall p, w#>(reg p) = stack_enc (v#>p).

  (* i is the position in the source code *)

  Definition bsm_instr_compile lnk i ii :=
    match ii with
      | PUSH s Zero => mm_push_Zero (reg s) tmp1 tmp2 (lnk i)
      | PUSH s One  => mm_push_One  (reg s) tmp1 tmp2 (lnk i)
      | POP  s j k  => mm_pop (reg s) tmp1 tmp2 (lnk i) (lnk j) (lnk (1+i)) (lnk k)
    end.

  Definition bsm_instr_compile_length (ii : bsm_instr m) :=
    match ii with
      | PUSH _ Zero => 7
      | PUSH _ One  => 8
      | POP  _ _ _  => 16
    end.

  Fact bsm_instr_compile_length_eq lnk i ii : length (bsm_instr_compile lnk i ii) = bsm_instr_compile_length ii.
  Proof. destruct ii as [ | ? [] ]; simpl; auto. Qed.

  Fact bsm_instr_compile_length_geq ii : 1 <= bsm_instr_compile_length ii.
  Proof. destruct ii as [ | ? [] ]; simpl; auto; lia. Qed.

  Hint Resolve bsm_instr_compile_length_eq bsm_instr_compile_length_geq : core.

  (* This main soundness lemma per simulated instruction *)

  Lemma bsm_instr_compile_sound : instruction_compiler_sound bsm_instr_compile (@bsm_sss _) (@mm_sss _) bsm_state_enc.
  Proof.
    intros lnk I i1 v1 i2 v2 w1 H; revert H w1.
    change v1 with (snd (i1,v1)) at 2.
    change i1 with (fst (i1,v1)) at 2 3 4 6 7 8.
    change v2 with (snd (i2,v2)) at 2.
    change i2 with (fst (i2,v2)) at 2.
    generalize (i1,v1) (i2,v2); clear i1 v1 i2 v2.
    induction 1 as    [ i p j k v Hv
                      | i p j k v ll Hll
                      | i p j k v ll Hll
                      | i p [] v
                      ]; simpl; intros w1 H0 H; generalize H; intros (H1 & H2 & H3).

    + exists w1; split; auto.
      apply mm_pop_void_progress; auto using Hv12, Hvr1, Hvr2.
      rewrite H3, Hv; auto.

    + exists (w1[(stack_enc ll)/reg p]); repeat split; auto; rew vec.
      * apply mm_pop_Zero_progress; auto using Hv12, Hvr1, Hvr2.
        rewrite H3, Hll; auto.
      * intros q; dest p q.
        assert (reg p <> reg q); rew vec.

    + exists (w1[(stack_enc ll)/reg p]); repeat split; auto; rew vec.
      * apply mm_pop_One_progress; auto using Hv12, Hvr1, Hvr2.
        rewrite H3, Hll; auto.
      * intros q; dest p q.
        assert (reg p <> reg q); rew vec.

    + exists (w1[(stack_enc (One::v#>p))/reg p]); repeat split; auto; rew vec.
      rewrite H0; apply mm_push_One_progress; auto using Hv12, Hvr1, Hvr2.
      intros q; dest p q.
      assert (reg p <> reg q); rew vec.

    + exists (w1[(stack_enc (Zero::v#>p))/reg p]); repeat split; auto; rew vec.
      rewrite H0; apply mm_push_Zero_progress; auto using Hv12, Hvr1, Hvr2.
      intros q; dest p q.
      assert (reg p <> reg q); rew vec.
  Qed.

  Hint Resolve bsm_instr_compile_sound : core.

  Section bsm_sim.

    Variable (iP : nat) (cP : list (bsm_instr m)).

    Local Definition lnk_Q_pair := @gen_compiler_correction _ _ _ _ bsm_instr_compile_length_eq _ _ _ _  (@bsm_sss_total' _)
                     (@mm_sss_fun _) _ bsm_instr_compile_sound (iP,cP) 1.

    Local Definition lnk := projT1 lnk_Q_pair.
    Local Definition Q := proj1_sig (projT2 lnk_Q_pair).

    Local Lemma Hlnk : fst Q = 1 /\ lnk iP = 1 /\ forall i, out_code i (iP,cP) -> lnk i = code_end Q.
    Proof.
      repeat split; apply (proj2_sig (projT2 lnk_Q_pair)).
    Qed.

    Infix "⋈" := bsm_state_enc (at level 70, no associativity).

    Local Lemma HQ1 : forall i1 v1 w1 i2 v2, v1 ⋈ w1 /\ (iP,cP) /BSM/ (i1,v1) ~~> (i2,v2)
                    -> exists w2,    v2 ⋈ w2 /\ Q /MM/ (lnk i1,w1) ~~> (lnk i2,w2).
    Proof. apply (proj2_sig (projT2 lnk_Q_pair)). Qed.

    Local Lemma HQ2 : forall i1 v1 w1 j2 w2, v1 ⋈ w1 /\ Q /MM/ (lnk i1,w1) ~~> (j2,w2)
                    -> exists i2 v2, v2 ⋈ w2 /\ (iP,cP) /BSM/ (i1,v1) ~~> (i2,v2) /\ j2 = lnk i2.
    Proof. apply (proj2_sig (projT2 lnk_Q_pair)). Qed.

    Variable v : vec (list bool) m.

    Local Definition w := 0##0##vec_map stack_enc v.

    Let w_prop : bsm_state_enc v w.
    Proof.
      red; unfold w, tmp1, tmp2; repeat split; rew vec.
      intros p; unfold reg; simpl.
      rewrite vec_pos_map; trivial.
    Qed.

    (* (iQ,cQ) simulates termination of (iP,cP) while ensuring tmp1 and tmp2 stay void when it terminates *)

    Local Lemma Q_spec1 : (iP,cP) /BSM/ (iP,v) ↓ -> exists w', Q /MM/ (1,w) ~~> (code_end Q, w') /\ w'#>tmp1 = 0 /\ w'#>tmp2 = 0.
    Proof.
      intros ((i1,v1) & H1).
      destruct HQ1 with (1 := conj w_prop H1) as (w' & H2 & H3).
      rewrite <- (proj2 (proj2 Hlnk) i1), <- (proj1 (proj2 Hlnk)).
      * exists w'; split; auto; red in H2; tauto.
      * apply H1.
    Qed.

    Local Lemma Q_spec2 : Q /MM/ (1,w) ↓ -> (iP,cP) /BSM/ (iP,v) ↓.
    Proof.
      intros ((j,w2) & H1).
      rewrite <- (proj1 (proj2 Hlnk)) in H1.
      destruct HQ2 with (1 := conj w_prop H1) as (i2 & v2 & H2 & H3 & _).
      exists (i2,v2); auto.
    Qed.

    Local Definition bsm_mm_sim := snd Q.

    Theorem bsm_mm_sim_spec : (iP,cP) /BSM/ (iP,v) ↓ <-> (1,bsm_mm_sim) /MM/ (1,w) ↓.
    Proof.
      rewrite <- (proj1 Hlnk) at 1.
      rewrite <- surjective_pairing.
      split; auto using Q_spec2.
      intros H.
      destruct (Q_spec1 H) as (w' & H1 & _).
      exists (code_end Q, w'); auto.
    Qed.

    Local Definition iE := code_end Q.

    (* We complete (iQ,cQ) with some code nullifying all variables except tmp1 & tmp2 *)

    Local Definition cN := mm_nullify tmp1 iE (map (fun p => pos_nxt (pos_nxt p)) (pos_list m)).
    Local Definition cE := cN ++ DEC tmp1 0 :: nil.

    Local Lemma E_spec w' : w'#>tmp1 = 0 -> w'#>tmp2 = 0 -> (iE,cE) /MM/ (iE,w') -+> (0,vec_zero).
    Proof.
      intros H1 H2.
      unfold cE.
      apply sss_compute_progress_trans with (length cN+iE,vec_zero).
      + apply subcode_sss_compute with (P := (iE,cN)); auto.
        apply mm_nullify_compute; auto.
        * intros p Hp.
          apply in_map_iff in Hp.
          destruct Hp as (x & H3 & H4); subst; discriminate.
        * intros p Hp.
          apply in_map_iff in Hp.
          destruct Hp as (x & H3 & H4); subst; apply vec_zero_spec.
        * intros p Hp.
          unfold n, tmp1, tmp2 in *; simpl in p.
          pos_inv p; auto.
          pos_inv p; auto.
          destruct Hp; apply in_map_iff; exists p; split; auto.
          apply pos_list_prop.
      + apply subcode_sss_progress with (P := (length cN+iE,DEC tmp1 0::nil)); auto.
        mm sss DEC zero with tmp1 0.
        apply subcode_refl.
        mm sss stop.
    Qed.

    Definition bsm_mm := snd Q ++ cE.

    Let cQ_sim : Q <sc (1,bsm_mm).
    Proof.
      pose proof Hlnk as Hlnk.
      unfold bsm_mm; destruct Q as (iQ,cQ); simpl in Hlnk.
      simpl snd; rewrite (proj1 Hlnk); auto.
    Qed.

    Let cE_sim : (iE,cE) <sc (1,bsm_mm).
    Proof.
      unfold iE, bsm_mm; subcode_tac; solve list eq.
      rewrite (proj1 Hlnk); auto.
    Qed.

    (* (1,bsm_sim) is a simulator for (iP,cP) *)

    Theorem bsm_mm_spec : (iP,cP) /BSM/ (iP,v) ↓ <-> (1,bsm_mm) /MM/ (1,w) ~~> (0,vec_zero).
    Proof.
      split.
      * intros H1.
        apply Q_spec1 in H1.
        destruct H1 as (w' & (H1 & H0) & H2 & H3).
        split.
        2: simpl; lia.
        apply sss_compute_trans with (st2 := (iE,w')).
        revert H1; apply subcode_sss_compute; auto.
        apply sss_progress_compute.
        generalize (E_spec _ H2 H3); apply subcode_sss_progress; auto.
      * intros H1.
        apply Q_spec2.
        apply subcode_sss_terminates with (1 := cQ_sim).
        exists (0,vec_zero); auto.
    Qed.

  End bsm_sim.

End simulator.

Theorem bsm_mm_compiler_1 n i (P : list (bsm_instr n)) :
  { Q : list (mm_instr (pos (2+n))) | forall v, (i,P) /BSM/ (i,v) ↓ <-> (1,Q) /MM/ (1,0##0##vec_map stack_enc v) ↓ }.
Proof. exists (bsm_mm_sim i P); apply bsm_mm_sim_spec. Qed.

Theorem bsm_mm_compiler_2 n i (P : list (bsm_instr n)) :
  { Q : list (mm_instr (pos (2+n))) | forall v, (i,P) /BSM/ (i,v) ↓ <-> (1,Q) /MM/ (1,0##0##vec_map stack_enc v) ~~> (0,vec_zero) }.
Proof. exists (bsm_mm i P); apply bsm_mm_spec. Qed.

author: uds-psl

repo: coq-synthetic-incompleteness


text:
(** * Programa\u00e7\u00e3o funcional em Coq *)

(* ############################################### *)
(** * Instala\u00e7\u00e3o *)

(** Passo-a-passo:
  1. Instalar OPAM: gerenciador de pacotes OCaml
  [passo j\u00e1 realizado pelo helpdesk no G3]
  Link: http://opam.ocaml.org/doc/Install.html
  a) wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin

  2. Instalar Coq 8.8.1
  Link: https://coq.inria.fr/opam/www/using.html
  a) abrir o terminal (ctrl + alt + t)
  b) export OPAMROOT=~/opam-coq.8.8.1
     # diret\u00f3rio de instala\u00e7\u00e3o no home do usu\u00e1rio
  c) opam init -n --comp=4.02.3 -j 4
     # 4 \u00e9 o n\u00famero de n\u00facleos de processamento
  d) opam repo add coq-released http://coq.inria.fr/opam/released
  e) opam install coq.8.8.1 && opam pin add coq 8.8.1

  3. Instalar CoqIDE
  Link: https://coq.inria.fr/opam/www/using.html
  a) opam install coqide

  4. Para rodar a IDE, \u00e9 preciso reexecutar os
  seguintes comandos sempre que abrir um novo
  terminal:
  a) abrir o terminal (ctrl + alt + t)
  b) export OPAMROOT=~/opam-coq.8.8.1
     # diret\u00f3rio em que instalou Coq
  c) eval `opam config env`
     # configurar ambiente
  d) coqide &

  5. Para testar a instala\u00e7\u00e3o, abrir o arquivo
  01-introducao-exemplo.v e process\u00e1-lo at\u00e9 o final
  (ctrl + end). O texto deve ficar todo verde.

  Outra op\u00e7\u00e3o de IDE: Emacs + ProofGeneral
  Link: https://proofgeneral.github.io/

  Links \u00fateis:
  - https://github.com/coq/coq
  - https://github.com/coq/coq/wiki
  - https://github.com/coq/coq/wiki/The-Coq-FAQ
*)

(* ############################################### *)
(** * Pref\u00e1cio *)

(** Material baseado na s\u00e9rie Software Foundations
    https://softwarefoundations.cis.upenn.edu/. *)

(** Aspectos centrais deste material:
    - uso de l\u00f3gica para definir e provar
      afirma\u00e7\u00f5es precisas sobre programas
    - uso de um assistente de prova (Coq)
      para construir argumentos l\u00f3gicos rigorosos
    - programa\u00e7\u00e3o funcional como liga\u00e7\u00e3o
      entre programa\u00e7\u00e3o e l\u00f3gica *)

(** Coq: aspectos hist\u00f3ricos
    - Em desenvolvimento deste 1984
    - Poss\u00edveis origens do nome:
      - Tradi\u00e7\u00e3o francesa: Caml, Elan, PhoX, etc.
      - Calculus of Constructions
      - S\u00edmbolo nacional da Fran\u00e7a
      - Primeiras tr\u00eas letras de Thierry Coquand *)

(** Coq: aplica\u00e7\u00f5es em CS e matem\u00e1tica:
    - Plataforma para modelar PLs
      [instru\u00e7\u00f5es x86, C, etc.]
    - Ambiente para desenvolver HW/SW certificado
      [CompCert, CertiKos, RISC-V, etc.]
    - Ambiente para programa\u00e7\u00e3o funcional
      [Gallina]
    - Assistente de prova para l\u00f3gica de alta ordem
      [Primeira prova verificada formalmente
       do Teorema das 4 cores] *)

(* ############################################### *)
(** * Gallina: introdu\u00e7\u00e3o *)

(** Definindo novo tipo: conjunto de valores poss\u00edveis.
    - [day] \u00e9 o nome do tipo
    - a defini\u00e7\u00e3o [day] \u00e9 um elemento de [Type]
    - [:=] usado para preceder a defini\u00e7\u00e3o
    - [|] \u00e9 usado para separar elementos de [day]
*)

Inductive day : Type :=
  | monday    : day
  | tuesday   : day
  | wednesday : day
  | thursday  : day
  | friday    : day
  | saturday  : day
  | sunday    : day.

(** Definindo uma fun\u00e7\u00e3o que opera sobre dias.
    - [Definition] fun\u00e7\u00f5es n\u00e3o-recursivas
    - Tipos n\u00e3o precisam ser expl\u00edcitos
    - [:=] precede a defini\u00e7\u00e3o da fun\u00e7\u00e3o
    - A defini\u00e7\u00e3o pode ser feita por casamento
      de padr\u00e3o, como tamb\u00e9m chamada a outras fun\u00e7\u00f5es
    - [=>] representa o retorno quando [d]
      casa com uma das op\u00e7\u00f5es
 *)

Definition next_weekday (d:day) : day :=
  match d with
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => monday
  | saturday  => monday
  | sunday    => monday
  end.

(** Validando a fun\u00e7\u00e3o definida:
    - [Compute]: avalia express\u00e3o
    - [Example]: define afirma\u00e7\u00e3o a ser verificada
      a) d\u00e1 um nome \u00e0 afirma\u00e7\u00e3o
      b) permite usar o modo de prova de Coq
         para verificar que a afirma\u00e7\u00e3o
         \u00e9 verdadeira (como um teste unit\u00e1rio)
    - Extrair programa funcional em OCaml ou Haskell
*)

Compute (next_weekday friday).
(* ==> monday : day *)

Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.

(** **** Exercise: (sinal) *)
(** Defina o tipo [sinal] que pode ser verde,
    amarelo ou vermelho. *)

(** **** Exercise: (next_sinal) *)
(** Defina a fun\u00e7\u00e3o [next_sinal] que muda a cor
    de um sinal para a pr\u00f3xima cor esperada *)

(** **** Exercise: (compute_sinal) *)
(** Use [Compute] para testar a defini\u00e7\u00e3o
    de [next_sinal]. *)

(** **** Exercise: (test_sinal) *)
(** Use [Example] para testar a defini\u00e7\u00e3o
    de [next_sinal]. Prove que sua
    afirma\u00e7\u00e3o \u00e9 verdadeira usando simpl.
    e reflexivity. *)

Inductive sinal : Type :=
  | verde : sinal
  | amarelo : sinal
  | vermelho : sinal.

Definition next_sinal (s:sinal) : sinal :=
  match s with
  | vermelho => amarelo
  | amarelo => verde
  | verde => vermelho
  end.

Compute (next_sinal vermelho).

Example test_sinal:
  (next_sinal (next_sinal vermelho)) = verde.
Proof. simpl. reflexivity. Qed.

(* =============================================== *)
(** ** Booleans *)

(** De forma similar, podemos definir o tipo booleano.
    - N\u00e3o confundir: booleano vs. True e False da l\u00f3gica *)

Inductive bool : Type :=
  | true : bool
  | false : bool.

(** Definindo fun\u00e7\u00f5es sobre booleanos
    - Observe a sintaxe para v\u00e1rios par\u00e2metros *)

Definition negb (b:bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.

Definition orb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

(** Teste unit\u00e1rios *)

Example test_orb1:  (orb true  false) = true.
Proof. simpl. reflexivity.  Qed.

Example test_orb2:  (orb false false) = false.
Proof. simpl. reflexivity.  Qed.

Example test_orb3:  (orb false true)  = true.
Proof. simpl. reflexivity.  Qed.

Example test_orb4:  (orb true  true)  = true.
Proof. simpl. reflexivity.  Qed.

(** \u00c9 poss\u00edvel definir uma sintaxe mais familiar
    usando [Notation] *)

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).

Example test_orb5:  false || false || true = true.
Proof. simpl. reflexivity. Qed.

(** **** Exercise: (nandb) *)
(** Defina nandb (usando casamento de padr\u00e3o e,
    em seguida, complete os testes unit\u00e1rios. *)

Definition nandb (b1:bool) (b2:bool) : bool :=
  match b1, b2 with
  | true, true => false
  | _, _ => true
  end.

Example test_nandb1:
(nandb true false) = true.
Proof. simpl. reflexivity.  Qed.

Example test_nandb2:
(nandb false false) = true.
Proof. simpl. reflexivity.  Qed.

Example test_nandb3:
(nandb false true) = true.
Proof. simpl. reflexivity.  Qed.

Example test_nandb4:
(nandb true true) = false.
Proof. simpl. reflexivity.  Qed.

(** **** Exercise: (nandb') *)
(** Defina nandb' usando as defini\u00e7\u00f5es [andb] e [negb] *)

Definition nandb' (b1:bool) (b2:bool) : bool
  (* SUBSTITUA COM ":= _sua_defini\u00e7\u00e3o_ ." *). Admitted.

(** Nas pr\u00f3ximas provas, observe o resultado do
    simpl. Tente antes desta t\u00e1tica, usar
    unfold nandb' (que obriga a expans\u00e3o da defini\u00e7\u00e3o
    de nandb'). *)

Example test_nandb'1:
(nandb' true false) = true.
(* COMPLETE AQUI *) Admitted.
Example test_nandb'2:
(nandb' false false) = true.
(* COMPLETE AQUI *) Admitted.
Example test_nandb'3:
(nandb' false true) = true.
(* COMPLETE AQUI *) Admitted.
Example test_nandb'4:
(nandb' true true) = false.
(* COMPLETE AQUI *) Admitted.

(** **** Exercise: (andb3)  *)
(** Defina a fun\u00e7\u00e3o [andb3]. Esta fun\u00e7\u00e3o deve
    retornar [true] quando todas suas entradas
    s\u00e3o [true], e [false] caso contr\u00e1rio *)

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool
  (* SUBSTITUA COM ":= _sua_defini\u00e7\u00e3o_ ." *). Admitted.

Example test_andb31:
(andb3 true true true) = true.
(* COMPLETE AQUI *) Admitted.
Example test_andb32:
(andb3 false true true) = false.
(* COMPLETE AQUI *) Admitted.
Example test_andb33:
(andb3 true false true) = false.
(* COMPLETE AQUI *) Admitted.
Example test_andb34:
(andb3 true true false) = false.
(* COMPLETE AQUI *) Admitted.

(* =============================================== *)
(** ** Function Types *)

(** Toda express\u00e3o em Coq tem um tipo. O comando
    [Check] imprime o tipo de uma express\u00e3o. *)

Check true.
(* ===> true : bool *)
Check (negb true).
(* ===> negb true : bool *)

(** A fun\u00e7\u00e3o [negb] \u00e9 tamb\u00e9m o valor de um dado, assim
    como [true] e [false]. Seu tipo \u00e9 chamado
    _function types_, e escrito usando setas *)

Check negb.
(* ===> negb : bool -> bool *)

(** [negb] \u00e9 uma fun\u00e7\u00e3o que dado um [bool],
    produz um [bool]. *)

Check andb.
(* ===> andb : bool -> bool -> bool *)

(** [andb] \u00e9 uma fun\u00e7\u00e3o que a partir de dois [bool],
    produz um [bool]. *)

(* =============================================== *)
(** ** Tipos compostos *)

(** Tipos definidos at\u00e9 ent\u00e3o: enumera\u00e7\u00f5es. Cada op\u00e7\u00e3o
    criada a partir de um certo _construtor_. *)

Inductive rgb : Type :=
  | red   : rgb
  | green : rgb
  | blue  : rgb.

(** A defini\u00e7\u00e3o a seguir possui o construtor [primary]
    que recebe um [rgb] e produz um [color]. *)

Inductive color : Type :=
  | black     : color
  | white     : color
  | primary   : rgb -> color.

Check black.

Check primary.

(** Definindo fun\u00e7\u00f5es sobre tipos compostos *)

Definition monochrome (c : color) : bool :=
  match c with
  | black     => true
  | white     => true
  | primary p => false
  end.

Definition isred (c : color) : bool :=
  match c with
  | black       => false
  | white       => false
  | primary red => true
  | primary _   => false
  end.

(** No exemplo acima, [primary _] tem o mesmo
    efeito de [primary p]. *)

(* =============================================== *)
(** ** M\u00f3dulos *)

(** Uma das maneiras de estruturar uma especifica\u00e7\u00e3o
    em Coq \u00e9 usar m\u00f3dulos. *)

Module NatPlayground.

(* =============================================== *)
(** ** N\u00fameros *)

(** Definindo um tipo usando construtores que recebem
    argumentos do tipo sendo definido. *)

(** N\u00fameros naturais
    - O: uma representa\u00e7\u00e3o do n\u00famero zero
    - S _: o sucessor de um n\u00famero natural *)

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

(** Por isso que tipos s\u00e3o (potencialmente) indutivos:
    - [O] \u00e9 um n\u00famero natural
    - [S O] \u00e9 um n\u00famero natural
    - [S (S O)] \u00e9 um n\u00famero natural
    - [S (S false)] n\u00e3o \u00e9 um n\u00famero natural *)

(** Esta defini\u00e7\u00e3o \u00e9 uma representa\u00e7\u00e3o estrutural
    sem significado. O significado vem do seu uso *)

Inductive nat' : Type :=
  | stop : nat'
  | tick : nat' -> nat'.

(** Exemplo: fun\u00e7\u00e3o [pred] *)

Definition pred (n : nat) : nat :=
  match n with
  | O     => O
  | S n'  => n'
  end.

End NatPlayground.

(** Coq possui defini\u00e7\u00f5es para representar
    n\u00fameros de forma decimal *)

Check (S (S (S (S O)))).
(* ===> 4 : nat *)

(** Definindo a fun\u00e7\u00e3o [minustwo]. Observe
    os dois primeiros casos *)

Definition minustwo (n : nat) : nat :=
  match n with
  | O => O
  | S O => O
  | S (S n') => n'
  end.

Compute (minustwo 4).
(* ===> 2 : nat *)

Compute (minustwo 1).
(* ===> 0 : nat *)

(** Tipos dos construtores e das fun\u00e7\u00f5es
    para [nat] *)

Check S.
Check pred.
Check minustwo.

(** Apesar de todos serem valores, as duas
    \u00faltimas defini\u00e7\u00f5es possuem uma no\u00e7\u00e3o
    de computabilidade associada *)

(** Definindo fun\u00e7\u00f5es recursivas: [Fixpoint]. *)

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb n'
  end.

(** Definindo [oddb] em fun\u00e7\u00e3o de [evenb] e [negb]. *)

Definition oddb (n:nat) : bool := negb (evenb n).

Example test_oddb1:    oddb 1 = true.
Proof. unfold oddb. simpl. reflexivity.  Qed.
Example test_oddb2:    oddb 4 = false.
Proof. simpl. reflexivity.  Qed.

(** Definindo fun\u00e7\u00f5es recursivas com
    v\u00e1rios par\u00e2metros *)

Module NatPlayground2.

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus n' m)
  end.

(** Testando a defini\u00e7\u00e3o *)
Compute (plus 3 2).
(* ===> 5 : nat *)

(** O passo-a-passo da computa\u00e7\u00e3o seria: *)

(*  [plus (S (S (S O))) (S (S O))]
==> [S (plus (S (S O)) (S (S O)))]
      pela segunda cl\u00e1sula do [match]
==> [S (S (plus (S O) (S (S O))))]
      pela segunda cl\u00e1sula do [match]
==> [S (S (S (plus O (S (S O)))))]
      pela segunda cl\u00e1sula do [match]
==> [S (S (S (S (S O))))]
      pela primeira cl\u00e1sula do [match]
*)

(** Outra nota\u00e7\u00e3o para v\u00e1rios par\u00e2metros
    do mesmo tipo *)

Fixpoint mult (n m : nat) : nat :=
  match n with
  | O => O
  | S n' => plus m (mult n' m)
  end.

Example test_mult1: (mult 3 3) = 9.
Proof. simpl. reflexivity.  Qed.

(** Casamento de padr\u00e3o m\u00faltiplo *)

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | O   , _    => O
  | S _ , O    => n
  | S n', S m' => minus n' m'
  end.

End NatPlayground2.

(** Definindo exponencia\u00e7\u00e3o: [exp] *)

Fixpoint exp (base power : nat) : nat :=
  match power with
  | O   => S O
  | S p => mult base (exp base p)
  end.

(** **** Exercise: 1(factorial)  *)
(** Defina a fun\u00e7\u00e3o fatorial em Coq
       factorial(0)  =  1
       factorial(n)  =  n * factorial(n-1)
                        (if n>0) *)

Fixpoint factorial (n:nat) : nat
  (* SUBSTITUA COM ":= _sua_defini\u00e7\u00e3o_ ." *). Admitted.

Example test_factorial1:
(factorial 3) = 6.
(* COMPLETE AQUI *) Admitted.

Example test_factorial2:
(factorial 5) = (mult 10 12).
(* COMPLETE AQUI *) Admitted.

(** As pr\u00f3ximas defini\u00e7\u00f5es definem uma sintaxe
    para adi\u00e7\u00e3o, subtra\u00e7\u00e3o e multiplica\u00e7\u00e3o
    - preced\u00eancia: [at level n], onde n 0..100
      menor valor indica maior preced\u00eancia
    - associatividade: [left], [right] ou
                       [no] [associativity]
 *)

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.

Notation "x - y" := (minus x y)
                       (at level 50, left associativity)
                       : nat_scope.

Notation "x * y" := (mult x y)
                       (at level 40, left associativity)
                       : nat_scope.

Check ((0 + 1) + 1).

(** Definindo se dois n\u00fameros s\u00e3o iguais: [beq_nat] *)

Fixpoint beq_nat (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => beq_nat n' m'
            end
  end.

(** Definindo menor ou igual: [leb] *)

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
  end.

Example test_leb1: (leb 2 2) = true.
Proof. simpl. reflexivity.  Qed.

Example test_leb2: (leb 2 4) = true.
Proof. simpl. reflexivity.  Qed.

Example test_leb3: (leb 4 2) = false.
Proof. simpl. reflexivity.  Qed.

(** **** Exercise: (blt_nat)  *)
(** A fun\u00e7\u00e3o [blt_nat] testa se um n\u00famero \u00e9
    menor do que outro. Observe que a pr\u00f3xima
    defini\u00e7\u00e3o n\u00e3o \u00e9 recursiva. \u00c9 preciso definir
    [blt_nat] a partir de defini\u00e7\u00f5es passadas *)

Definition blt_nat (n m : nat) : bool
  (* SUBSTITUA COM ":= _sua_defini\u00e7\u00e3o_ ." *). Admitted.

Example test_blt_nat1:
(blt_nat 2 2) = false.
(* COMPLETE AQUI *) Admitted.

Example test_blt_nat2:
(blt_nat 2 4) = true.
(* COMPLETE AQUI *) Admitted.

Example test_blt_nat3:
(blt_nat 4 2) = false.
(* COMPLETE AQUI *) Admitted.

(* ############################################### *)
(** * Leitura sugerida *)

(** Software Foundations: volume 1
  - Pref\u00e1cio
  https://softwarefoundations.cis.upenn.edu/lf-current/Preface.html
  - Aspectos b\u00e1sicos (at\u00e9 o final de "Data and Functions")
  https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html
*)

author: marcosmmb


text:
(** * Maps: Total and Partial Maps *)

(** _Maps_ (or _dictionaries_) are ubiquitous data structures both
    generally and in the theory of programming languages in
    particular; we're going to need them in many places in the coming
    chapters.  They also make a nice case study using ideas we've seen
    in previous chapters, including building data structures out of
    higher-order functions (from [Basics] and [Poly]) and the use of
    reflection to streamline proofs (from [IndProp]).

    We'll define two flavors of maps: _total_ maps, which include a
    "default" element to be returned when a key being looked up
    doesn't exist, and _partial_ maps, which return an [option] to
    indicate success or failure.  The latter is defined in terms of
    the former, using [None] as the default element. *)

(* ################################################################# *)
(** * The Coq Standard Library *)

(** One small digression before we get to maps.

    Unlike the chapters we have seen so far, this one does not
    [Require Import] the chapter before it (and, transitively, all the
    earlier chapters).  Instead, in this chapter and from now, on
    we're going to import the definitions and theorems we need
    directly from Coq's standard library stuff.  You should not notice
    much difference, though, because we've been careful to name our
    own definitions and theorems the same as their counterparts in the
    standard library, wherever they overlap. *)

Require Import Coq.Arith.Arith.
Require Import Coq.Bool.Bool.
Require Import Coq.Strings.String.
Require Import Coq.Logic.FunctionalExtensionality.

(** Documentation for the standard library can be found at
    http://coq.inria.fr/library/.

    The [Search] command is a good way to look for theorems involving
    objects of specific types.  Take a minute now to experiment with it. *)

(* ################################################################# *)
(** * Identifiers *)

(** First, we need a type for the keys that we use to index into our
    maps.  For this purpose, we again use the type [id] from the
    [Lists] chapter.  To make this chapter self contained, we repeat
    its definition here, together with the equality comparison
    function for [id]s and its fundamental property. *)

Inductive id : Type :=
  | Id : string -> id.

Definition beq_id x y :=
  match x,y with
    | Id n1, Id n2 => if string_dec n1 n2 then true else false
  end.

(** (The function [string_dec] comes from Coq's string library.
    If you check its result type, you'll see that it does not actually
    return a [bool], but rather a type that looks like [{x = y} + {x
    <> y}], called a [sumbool], which can be thought of as an
    "evidence-carrying boolean."  Formally, an element of [sumbool] is
    either a proof that two things are equal or a proof that they are
    unequal, together with a tag indicating which.  But for present
    purposes you can think of it as just a fancy [bool].) *)

Theorem beq_id_refl : forall id, true = beq_id id id.
Proof.
  intros [n]. simpl. destruct (string_dec n n).
  - reflexivity.
  - destruct n0. reflexivity.
Qed.

(** The following useful property of [beq_id] follows from an
    analogous lemma about strings: *)

Theorem beq_id_true_iff : forall x y : id,
  beq_id x y = true <-> x = y.
Proof.
   intros [n1] [n2].
   unfold beq_id.
   destruct (string_dec n1 n2).
   - subst. split. reflexivity. reflexivity.
   - split.
     + intros contra. inversion contra.
     + intros H. inversion H. subst. destruct n. reflexivity.
Qed.

(** Similarly: *)

Theorem beq_id_false_iff : forall x y : id,
  beq_id x y = false
  <-> x <> y.
Proof.
  intros x y. rewrite <- beq_id_true_iff.
  rewrite not_true_iff_false. reflexivity. Qed.

(** This useful variant follows just by rewriting: *)

Theorem false_beq_id : forall x y : id,
   x <> y
   -> beq_id x y = false.
Proof.
  intros x y. rewrite beq_id_false_iff.
  intros H. apply H. Qed.

(* ################################################################# *)
(** * Total Maps *)

(** Our main job in this chapter will be to build a definition of
    partial maps that is similar in behavior to the one we saw in the
    [Lists] chapter, plus accompanying lemmas about its behavior.

    This time around, though, we're going to use _functions_, rather
    than lists of key-value pairs, to build maps.  The advantage of
    this representation is that it offers a more _extensional_ view of
    maps, where two maps that respond to queries in the same way will
    be represented as literally the same thing (the very same function),
    rather than just "equivalent" data structures.  This, in turn,
    simplifies proofs that use maps. *)

(** We build partial maps in two steps.  First, we define a type of
    _total maps_ that return a default value when we look up a key
    that is not present in the map. *)

Definition total_map (A:Type) := id -> A.

(** Intuitively, a total map over an element type [A] is just a
    function that can be used to look up [id]s, yielding [A]s. *)

(** The function [t_empty] yields an empty total map, given a default
    element; this map always returns the default element when applied
    to any id. *)

Definition t_empty {A:Type} (v : A) : total_map A :=
  (fun _ => v).

(** More interesting is the [update] function, which (as before) takes
    a map [m], a key [x], and a value [v] and returns a new map that
    takes [x] to [v] and takes every other key to whatever [m] does. *)

Definition t_update {A:Type} (m : total_map A)
                    (x : id) (v : A) :=
  fun x' => if beq_id x x' then v else m x'.

(** This definition is a nice example of higher-order programming:
    [t_update] takes a _function_ [m] and yields a new function
    [fun x' => ...] that behaves like the desired map.

    For example, we can build a map taking [id]s to [bool]s, where [Id
    "foo"] is mapped to [true] and every other key is mapped to [false],
    like this: *)

Definition examplemap :=
  t_update (t_update (t_empty false) (Id "foo") false)
           (Id "bar") true.

(** This completes the definition of total maps.  Note that we
    don't need to define a [find] operation because it is just
    function application! *)

Example update_example1 : examplemap (Id "baz") = false.
Proof. reflexivity. Qed.

Example update_example2 : examplemap (Id "foo") = false.
Proof. reflexivity. Qed.

Example update_example3 : examplemap (Id "quux") = false.
Proof. reflexivity. Qed.

Example update_example4 : examplemap (Id "bar") = true.
Proof. reflexivity. Qed.

(** To use maps in later chapters, we'll need several fundamental
    facts about how they behave. *)

(** Even if you don't work the following exercises, make sure
    you thoroughly understand the statements of the lemmas! *)

(** (Some of the proofs require the functional extensionality axiom,
    which is discussed in the [Logic] chapter.) *)

(** **** Exercise: 1 star, optional (t_apply_empty)  *)
(** First, the empty map returns its default element for all keys: *)

Lemma t_apply_empty:  forall A x v, @t_empty A v x = v.
Proof.
  unfold t_empty. intros A _ v. reflexivity.
Qed.
(** [] *)

(** **** Exercise: 2 stars, optional (t_update_eq)  *)
(** Next, if we update a map [m] at a key [x] with a new value [v]
    and then look up [x] in the map resulting from the [update], we
    get back [v]: *)

Lemma t_update_eq : forall A (m: total_map A) x v,
  (t_update m x v) x = v.
Proof.
  unfold t_update. intros A m x v.
  rewrite <- beq_id_refl. reflexivity.
Qed.
(** [] *)

(** **** Exercise: 2 stars, optional (t_update_neq)  *)
(** On the other hand, if we update a map [m] at a key [x1] and then
    look up a _different_ key [x2] in the resulting map, we get the
    same result that [m] would have given: *)

Theorem t_update_neq : forall (X:Type) v x1 x2
                         (m : total_map X),
  x1 <> x2 ->
  (t_update m x1 v) x2 = m x2.
Proof.
  intros X v x1 x2 m Hneq.
  unfold t_update. destruct (beq_id x1 x2) eqn:HE.
  - rewrite beq_id_true_iff in HE. exfalso. apply Hneq. apply HE.
  - reflexivity.
Qed.
(** [] *)

(** **** Exercise: 2 stars, optional (t_update_shadow)  *)
(** If we update a map [m] at a key [x] with a value [v1] and then
    update again with the same key [x] and another value [v2], the
    resulting map behaves the same (gives the same result when applied
    to any key) as the simpler map obtained by performing just
    the second [update] on [m]: *)

Lemma t_update_shadow : forall A (m: total_map A) v1 v2 x,
    t_update (t_update m x v1) x v2
  = t_update m x v2.
Proof.
  intros A m v1 v2 x. apply functional_extensionality. intros x'. unfold t_update.
  destruct (beq_id x x').
  - reflexivity. - reflexivity.
Qed.
(** [] *)

(** For the final two lemmas about total maps, it's convenient to use
    the reflection idioms introduced in chapter [IndProp].  We begin
    by proving a fundamental _reflection lemma_ relating the equality
    proposition on [id]s with the boolean function [beq_id]. *)

(** **** Exercise: 2 stars, optional (beq_idP)  *)
(** Use the proof of [beq_natP] in chapter [IndProp] as a template to
    prove the following: *)

Lemma beq_idP : forall x y, reflect (x = y) (beq_id x y).
Proof.
  intros x y. apply iff_reflect. destruct (beq_id x y) eqn:HE.
  - rewrite beq_id_true_iff in HE. split.
    + reflexivity. + intros _. apply HE.
  - rewrite beq_id_false_iff in HE. split.
    + intros H. exfalso. apply HE. apply H.
    + intros H. inversion H.
Qed.
(** [] *)

(** Now, given [id]s [x1] and [x2], we can use the [destruct (beq_idP
    x1 x2)] to simultaneously perform case analysis on the result of
    [beq_id x1 x2] and generate hypotheses about the equality (in the
    sense of [=]) of [x1] and [x2]. *)

(** **** Exercise: 2 stars (t_update_same)  *)
(** With the example in chapter [IndProp] as a template, use
    [beq_idP] to prove the following theorem, which states that if we
    update a map to assign key [x] the same value as it already has in
    [m], then the result is equal to [m]: *)

Theorem t_update_same : forall X x (m : total_map X),
  t_update m x (m x) = m.
Proof.
  intros X x m. apply functional_extensionality. intro x'. unfold t_update.
  destruct (beq_idP x x').
  - rewrite e. reflexivity. - reflexivity.
Qed.
(** [] *)

(** **** Exercise: 3 stars, recommended (t_update_permute)  *)
(** Use [beq_idP] to prove one final property of the [update]
    function: If we update a map [m] at two distinct keys, it doesn't
    matter in which order we do the updates. *)

Theorem t_update_permute : forall (X:Type) v1 v2 x1 x2
                             (m : total_map X),
  x2 <> x1 ->
    (t_update (t_update m x2 v2) x1 v1)
  = (t_update (t_update m x1 v1) x2 v2).
Proof.
  intros X v1 v2 x1 x2 m Hneq.
  apply functional_extensionality. intro x. unfold t_update.
  destruct (beq_idP x1 x).
  - destruct (beq_idP x2 x).
    + exfalso. apply Hneq. rewrite e,e0. reflexivity.
    + reflexivity.
  - destruct (beq_idP x2 x).
    + reflexivity.
    + reflexivity.
Qed.
(** [] *)

(* ################################################################# *)
(** * Partial maps *)

(** Finally, we define _partial maps_ on top of total maps.  A partial
    map with elements of type [A] is simply a total map with elements
    of type [option A] and default element [None]. *)

Definition partial_map (A:Type) := total_map (option A).

Definition empty {A:Type} : partial_map A :=
  t_empty None.

Definition update {A:Type} (m : partial_map A)
                  (x : id) (v : A) :=
  t_update m x (Some v).

(** We now straightforwardly lift all of the basic lemmas about total
    maps to partial maps.  *)

Lemma apply_empty : forall A x, @empty A x = None.
Proof.
  intros. unfold empty. rewrite t_apply_empty.
  reflexivity.
Qed.

Lemma update_eq : forall A (m: partial_map A) x v,
  (update m x v) x = Some v.
Proof.
  intros. unfold update. rewrite t_update_eq.
  reflexivity.
Qed.

Theorem update_neq : forall (X:Type) v x1 x2
                       (m : partial_map X),
  x2 <> x1 ->
  (update m x2 v) x1 = m x1.
Proof.
  intros X v x1 x2 m H.
  unfold update. rewrite t_update_neq. reflexivity.
  apply H. Qed.

Lemma update_shadow : forall A (m: partial_map A) v1 v2 x,
  update (update m x v1) x v2 = update m x v2.
Proof.
  intros A m v1 v2 x1. unfold update. rewrite t_update_shadow.
  reflexivity.
Qed.

Theorem update_same : forall X v x (m : partial_map X),
  m x = Some v ->
  update m x v = m.
Proof.
  intros X v x m H. unfold update. rewrite <- H.
  apply t_update_same.
Qed.

Theorem update_permute : forall (X:Type) v1 v2 x1 x2
                                (m : partial_map X),
  x2 <> x1 ->
    (update (update m x2 v2) x1 v1)
  = (update (update m x1 v1) x2 v2).
Proof.
  intros X v1 v2 x1 x2 m. unfold update.
  apply t_update_permute.
Qed.

(** $Date: 2017-08-24 17:13:02 -0400 (Thu, 24 Aug 2017) $ *)

author: Javran

repo: Thinking-dumps

save_path: github-repos/coq/Javran-Thinking-dumps


text:
Require Import language.
Require Import msl.base.
Require Import msl.seplog.
Require Import msl.alg_seplog.
Require Import seplogic.
Require Import lseg.
Require Import msl.Coqlib2.
Require Import msl.log_normalize.

Local Open Scope logic.

Import Semax.

(* PROOF AUTOMATION FOR SEMAX *)

Hint Extern 3 (inlist _ _ = false) => (compute; reflexivity).

Lemma arguments_gss: forall x xl v vl, arguments (x::xl)(v::vl) x = v.
Proof.
  intros.
 Transparent arguments. unfold arguments, locals2env,mk_locals;  simpl.
 Opaque arguments.
  rewrite if_true; auto.
Qed.
Lemma arguments_gso: forall x xl v vl x', x<>x' -> arguments (x::xl)(v::vl)x' = arguments xl vl x'.
Proof.
  intros.
 Transparent arguments. unfold arguments, locals2env,mk_locals;  simpl.
 Opaque arguments.
  rewrite if_false; auto.
Qed.

Ltac compute_neq := solve [let H := fresh in intro H; inversion H].

Hint Rewrite arguments_gss : args.
Hint Rewrite arguments_gso using compute_neq : args.

Ltac call_tac := unfold call; simpl; autorewrite with args; simpl.

Lemma funassert_e:  forall G i f,
      table_get G i = Some f ->
      funassert G |-- cont f i.
Proof.
  intros.
  unfold funassert.
  apply andp_left1.
  apply allp_left with i. apply allp_left with f.
  normalize.
  eapply derives_trans with (TT && (TT --> cont f i)).
  apply andp_right; auto. apply TT_right. apply modus_ponens.
Qed.

Ltac funassert_tac :=
  match goal with
  | |-   ?A && ?B |-- _ =>
      match A with context [funassert _] => apply andp_left1; funassert_tac  end ||
      match B with context [funassert _] => apply andp_left2; funassert_tac  end
  | |- funassert _ |-- _ => apply funassert_e; simpl; reflexivity
 end.

Ltac func_tac :=
   apply semax_func_cons;
    [ compute; reflexivity | compute; reflexivity | compute; reflexivity
    |  (*eapply semax_pre; [intro ; call_tac; apply derives_refl | ] *)
    | ].

Ltac rewrite' H := eapply semax_pre; [ intro; rewrite H; apply derives_refl | ].

(* This tactic works but introduces magic wands, which is undesirable *)
Ltac forward_magic :=
  match goal with |- semax _ ?G ?P (Assign (Mem ?e1) ?e2 ?c) =>
      let v := fresh "v" in
        (evar (v:adr);
       apply semax_pre with (P' := fun s => mapsto (eval e1 s) v * (mapsto (eval e1 s) v -* P s));
               [intro | apply semax_store; auto  ] );
       unfold v; clear v
  end.

Hint Resolve now_later sepcon_derives.

Definition semax_body (G: funspecs) (spec: funspec) (f: list var * control) :=
  semax (fst f) G (fun s => call spec (map s (fst f))) (snd f).

Lemma semax_store_next: forall x y v c vars G (Q P: assert),
    expcheck vars x = true ->
    expcheck vars y = true ->
    Q = (fun s => next (eval x s) v  * P s) ->
    semax vars G (fun s => next (eval x s) (eval y s) * P s) c ->
    semax vars G Q  (Do Mem x  := y ; c).
Proof. intros; subst.
    apply semax_pre with (fun s => mapsto (eval x s) v * (!! (eval x s > 0) && P s)).
    intros. unfold next. rewrite sepcon_andp_prop.
    rewrite sepcon_comm. rewrite sepcon_andp_prop. rewrite sepcon_comm; auto.
    apply semax_store; auto.
    eapply semax_pre; try apply H2.
    intros; unfold next.
    rewrite sepcon_andp_prop.
    rewrite (sepcon_comm (andp _ _)). rewrite sepcon_andp_prop.
   rewrite sepcon_comm; auto.
 Qed.

Lemma semax_load_next: forall x y z c vars G P,
    expcheck vars y = true ->
    semax (vs_add x vars) G P c ->
    semax vars G (fun s => (next (eval y s) z * TT) && |> subst x z P s)
               (Do x := Mem y ; c).
Proof.
 intros.
  apply semax_pre with (fun s => mapsto (eval y s) z * TT && |> subst x z P s).
 intros. apply andp_derives; auto. apply sepcon_derives; auto. apply andp_left2; auto.
 apply semax_load; auto.
Qed.

Ltac forward :=
 match goal with
 | |- semax _ _ _ (IfThenElse _ _ _) =>
          apply semax_if; [ compute; reflexivity | | ]
 | |- semax _ _ _ (Assign (Mem _) _ _) =>
            (eapply semax_store || eapply semax_store_next);
             [ compute ; reflexivity | compute; reflexivity | reflexivity | ]
 | |- semax _ _ _ (Assign _ (Mem _) _) =>
            (eapply semax_load || eapply semax_load_next);
             [ compute ; reflexivity | ]
 | |- semax _ _ ?P (Go ?x ?ys) =>
  apply semax_G;
  let p := fresh "P" in
   evar (p: funspec);
   eapply semax_pre with (fun s => cont p (eval x s) && call p (eval_list ys s));
       [ intro; apply andp_right
       | apply semax_go; [ compute; reflexivity ] ]; unfold p; clear p;
       [ try funassert_tac | call_tac  ]; simpl
 end.

author: PrincetonUniversity

repo: VST