diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 143 |
1 files changed, 137 insertions, 6 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index 0475f0451..78342238d 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -1618,9 +1618,54 @@ Module Fancy. Context (reg : Type) (error_reg : reg) (reg_eqb : reg -> reg -> bool). - - Lemma allocate_correct cc ctx e reg_list name_to_reg : - interp reg_eqb wordmax cc_spec (allocate reg name name_eqb error_reg e reg_list name_to_reg) cc ctx = interp name_eqb wordmax cc_spec e cc (fun n : name => ctx (name_to_reg n)). + Context (reg_eqb_refl : forall r, reg_eqb r r = true). + + Lemma interp_ctx_ext e : + forall cc ctx ctx', + (forall n, ctx n = ctx' n) -> + interp name_eqb wordmax cc_spec e cc ctx = interp name_eqb wordmax cc_spec e cc ctx'. + Proof. + induction e; intros; [ cbn; solve [auto] | ]. + cbn. erewrite Tuple.map_ext by eassumption. + apply IHe; [ ]. intros; break_innermost_match; eauto. + Qed. + + Fixpoint reg_depth {t} (e : @expr t) : nat := + match e with + | Ret _ => 0 + | Instr i rd args cont => S (reg_depth cont) + end. + Check interp. + + Lemma allocate_correct e : + forall cc ctx reg_list name_to_reg, + (reg_depth e <= length reg_list)%nat -> + interp reg_eqb wordmax cc_spec (allocate reg name name_eqb error_reg e reg_list name_to_reg) cc ctx + = interp name_eqb wordmax cc_spec e cc (fun n : name => ctx (name_to_reg n)). + Proof. + induction e; cbn [allocate]; intros; [ reflexivity | ]. + destruct reg_list; intros; cbn [reg_depth] in *; distr_length; [ ]. + cbn. rewrite IHe; try omega. + + + rewrite Tuple.map_map. + apply interp_ctx_ext; [ ]. intros. + break_innermost_match; try reflexivity. + rewrite reg_eqb_refl in *. congruence. + (* + TODO + name_to_reg is more or less the context -- names that have already been assigned to registers + rd : name (destination name) + n : name (input to ctx) + r : reg (register in which rd now goes) + + if n != rd then name_to_reg n != r? + + rd has been assigned to the name r. + It might be that r has a previous assignment (exists n, name_to_reg n = r and n != rd). + However, we can count on that n never being called, if the reg_list is okay. + *) + Admitted. End with_name. @@ -1801,6 +1846,52 @@ Module Fancy. [ rewrite H | apply in_app_or in H; destruct H ] end; eauto. } Qed. + + Section expression_equivalence. + Context {name1 name2} + (name1_eqb : name1 -> name1 -> bool) + (name2_eqb : name2 -> name2 -> bool) + (name1_eqb_eq : forall n m, name1_eqb n m = true -> n = m) + (name1_eqb_neq : forall n m, name1_eqb n m = false -> n <> m) + (name2_eqb_eq : forall n m, name2_eqb n m = true -> n = m) + (name2_eqb_neq : forall n m, name2_eqb n m = false -> n <> m). + + (* name1 should only map to a single name2; several name1s might map to the same name2 *) + Inductive in_step : (name1 -> name2) -> expr -> expr -> Prop := + | in_step_ret : + forall M n1 n2, M n1 = n2 -> in_step M (Ret n1) (Ret n2) + | in_step_instr : + forall i M rd1 rd2 args1 args2 e1 e2, + in_step M e1 e2 -> + Tuple.map M args1 = args2 -> (* args correspond with old assignments *) + M rd1 = rd2 -> (* destination register corresponds with new assignment *) + in_step M (Instr i rd1 args1 e1) (Instr i rd2 args2 e2) + . + + Lemma interp_eq M e1 e2 (HM : forall n n', M n = M n' -> n = n') : + in_step M e1 e2 -> + forall cc ctx1 ctx2, + (forall n1, ctx1 n1 = ctx2 (M n1)) -> + interp name1_eqb wordmax cc_spec e1 cc ctx1 = + interp name2_eqb wordmax cc_spec e2 cc ctx2. + Proof. + induction 1; intros; cbn [interp]; [ congruence | ]. + replace (Tuple.map ctx1 args1) with (Tuple.map ctx2 args2) + by (subst args2; rewrite Tuple.map_map; apply Tuple.map_ext_In; intros; + match goal with | H : context [ctx1 _ = ctx2 _] |- _ => rewrite H end; + f_equal; eauto using eq_sym). + apply IHin_step; intros; eauto. + break_innermost_match; + repeat match goal with + | _ => progress subst + | H : _ = true |- _ => apply name1_eqb_eq in H + | H : _ = false |- _ => apply name1_eqb_neq in H + | H : _ = true |- _ => apply name2_eqb_eq in H + | H : _ = false |- _ => apply name2_eqb_neq in H + | H : M _ = M _ |- _ => apply HM in H + end; congruence. + Qed. + End expression_equivalence. End Proofs. End Fancy. @@ -2447,7 +2538,8 @@ Module Barrett256. end. Local Opaque PreFancy.interp_cast_mod. - + *) + Lemma prod_barrett_red256_correct : forall (cc_start_state : Fancy.CC.state) (* starting carry flags *) (start_context : register -> Z) (* starting register values *) @@ -2468,13 +2560,52 @@ Module Barrett256. replace (2^machine_wordsize) with r in * by reflexivity. cbv [M muLow] in *. - rewrite <-barrett_red256_correct_full by auto. + erewrite <-barrett_red256_fancy_correct with (error:=100000%positive) by eauto. rewrite <-barrett_red256_alloc_equivalent with (errorR := RegZero) (errorP := 1%positive) (extra_reg:=extra_reg) by (auto; cbn; auto with omega). cbv [ProdEquiv.interp256]. let r := (eval compute in (2 ^ 256)) in replace (2^256) with r in * by reflexivity. - cbv [barrett_red256_alloc barrett_red256 expr.Interp]. + + cbn - [Fancy.interp Pos.eqb]. + cbv [Fancy.make_cc]. + match goal with |- _ = Fancy.interp _ _ _ _ ?cc _ => + let x := fresh in + set cc as x; cbv [Pos.eqb] in x; subst x + end. + assert (Fancy.CC.cc_m cc_start_state = Fancy.cc_spec Fancy.CC.M (start_context xHigh)) as M_equal. + { match goal with H : Fancy.CC.cc_m _ = _ |- _ => rewrite H end. + cbv [Fancy.cc_spec]. rewrite Z.cc_m_eq, Z.testbit_eqb by omega. + rewrite Z.mod_small by (split; [ solve [Z.zero_bounds] | apply Z.div_lt_upper_bound; cbn; omega ]). + reflexivity. } + rewrite <-M_equal. + + (* strategy to fix flags : + 1) replace state on both sides with a state reflecting dead flags updated to 0; prove that each side ignores those flags and interps remain equal + 2) prove that the M flags are the same and rewrite; now same flags are on both sides + *) + + let dead_flags := constr:([Fancy.CC.C; Fancy.CC.L; Fancy.CC.Z]) in + match goal with + | H : Fancy.CC.cc_m _ = _ + |- _ = Fancy.interp _ _ _ _ ?cc _ => + let x := fresh in + let Hx := fresh in + remember (Fancy.CC.update dead_flags 0 Fancy.cc_spec cc) as x eqn:Hx; + cbv [Fancy.CC.update] in Hx; cbn in Hx; + match goal with + |- ?lhs = ?rhs => + match (eval pattern cc in rhs) with + ?f _ => transitivity (f x); subst x + end + end + end. + + 2 : { + (* here's where we need to prove the interps are equal even if I change the dead flags *) + + + cbv [barrett_red256_alloc barrett_red256_fancy]. step start_context. { match goal with H : Fancy.CC.cc_m _ = _ |- _ => rewrite H end. |