Module ProductProof

Require Import Product.
Require RTLperm.
Require Import MoreRelations.
Import Utf8.
Import Coqlib.
Import Maps.
Import Util.
Import ShareTree TreeAl.
Import Sexpr.
Import Sylvie.
Import ToString.

Instance bool'_dec : EqDec bool := bool_dec.
Instance nat_dec : EqDec nat := eq_nat_dec.
Instance sig_dec : EqDec AST.signature := AST.signature_eq.
Instance condition_dec : EqDec Op.condition := Op.eq_condition.
Instance operation_dec : EqDec Op.operation := Op.eq_operation.
Instance external_function_dec : EqDec AST.external_function := AST.external_function_eq.

Instance option_dec {X: Type} `(EqDec X) : EqDec (option X) :=
  λ x x',
  match x, x' with
  | None, None => left eq_refl
  | Some o, Some o' =>
    match eq_dec o o' with left EQ => left (f_equal Some EQ) | right NE => right (λ K, NE (some_eq_inv K)) end
  | None, Some o' => right (λ K, None_not_Some K False)
  | Some o, None => right (λ K, None_not_Some (eq_sym K) False)
  end.

Inductive proof (P: Prop) : Set :=
| Proof `(P).
Arguments Proof [P] _.

Local Notation "[ P ]" := (proof P): type_scope.

Definition proof_of_proof {P: Prop} (p: proof P) : P :=
  let 'Proof H := p in H.

Unset Elimination Schemes.

Definition pc_triple : Type := (RTL.node * RTL.node * Sylvie.node)%type.

Module PPPTree : SHARETREE with Definition elt := pc_triple
  := ProdShareTree PPTree PShareTree.

Module PPPP := Tree_Properties PPPTree.

Section REGISTER.

Context (reg: Type).
Context (reg_dec: EqDec reg).
Context (left right: Registers.reg → reg).

Section RESULT.
Context
  (progL progR: RTL.code)
  (is_dead_branch: side → RTL.code → node → bool).

Context (predL predR: node → list node).

Context
  (prod: Sylvie.code reg)
  (ppmap: PPTree.t (list node))
  (deco: hashmap (decoration reg))
  (hints: PTree.t side).

Definition β (pcL pcR pc: node) : Prop :=
  match PPTree.get (pcL, pcR) ppmap with
  | None => False
  | Some pcs => In pc pcs
  end.

Definition δ (pc: node) (a: assertion reg) : Prop :=
  In a (get_assertions deco pc).

Definition match_single_instruction (reg: Registers.reg → reg)
           (i: RTL.instruction) (ie: node) (pc: node) (je: node) : Prop :=
  ∃ j, prod ! pc = Some j ∧
  match i, j with
  | RTL.Inop ie', Egoto je' => ie' = ie ∧ je' = je ∧ (pc <= je')%positive
  | RTL.Iop op args dst ie', Eop dst' op' args' je' =>
    ie' = ie ∧ je' = je ∧
    dst' = reg dst ∧ op' = Operation op ∧ args' = List.map reg args ∧
    is_dangerous_op op args = false
  | _, _ => False
  end.

Definition match_return (rL rR: option Registers.reg) (pc: node) : Prop :=
  match rL, rR with
  | Some vL, Some vR => δ pc (assert_eq_reg (left vL) (right vR))
  | None, None => Logic.True
  | _, _ => False
  end.

Definition match_builtin_args (pc: node) aL aR :=
  match aL, aR with
  | AST.BA r1, AST.BA r2 => δ pc (assert_eq_reg (left r1) (right r2))
  | AST.BA_int i1, AST.BA_int i2 => i1 = i2
  | AST.BA_addrglobal s1 o1, AST.BA_addrglobal s2 o2 => s1 = s2 ∧ o1 = o2
  | _, _ => False
  end.

Definition match_builtin_dst pc pc' dst1 dst2 :=
    match dst1, dst2 with
    | AST.BR x1, AST.BR x2 =>
      ∃ pci,
        prod ! pc = Some (Eop (left x1) Havoc nil pci) ∧
        prod ! pci = Some (Eop (right x2) (Operation Op.Omove) (left x1 :: nil) pc')
    | AST.BR_none, AST.BR_none => prod ! pc = Some (Egoto pc')
    | _, _ => False
    end.

Definition match_instructions_one
           (iL: RTL.instruction) (pcL': node)
           (iR: RTL.instruction) (pcR': node)
           (pc pc': node) : Prop :=
  match iL, iR with
  | RTL.Iop op1 args1 dst1 pc1', RTL.Iop op2 args2 dst2 pc2' =>
    op1 = op2 ∧
    pc1' = pcL' ∧
    pc2' = pcR' ∧
    Forall2 (λ aL aR, δ pc (assert_eq_reg (left aL) (right aR))) args1 args2 ∧
    ∃ pci,
    prod ! pc = Some (Eop (left dst1) (Operation op1) (List.map left args1) pci) ∧
    prod ! pci = Some (Eop (right dst2) (Operation Op.Omove) (left dst1 :: nil) pc')

  | RTL.Iload _ κ1 addr1 args1 dst1 pc1', RTL.Iload _ κ2 addr2 args2 dst2 pc2' =>
    κ1 = κ2 ∧
    pc1' = pcL' ∧
    pc2' = pcR' ∧
    δ pc (AssertEQ (addr addr1 left args1) (addr addr2 right args2)) ∧
    ∃ pci,
    prod ! pc = Some (Eop (left dst1) Havoc nil pci) ∧
    prod ! pci = Some (Eop (right dst2) (Operation Op.Omove) (left dst1 :: nil) pc')

  | RTL.Icall sg1 f1 args1 dst1 pc1', RTL.Icall sg2 f2 args2 dst2 pc2' =>
    sg1 = sg2 ∧
    pc1' = pcL' ∧
    pc2' = pcR' ∧
    Forall2 (λ aL aR, δ pc (assert_eq_reg (left aL) (right aR))) args1 args2 ∧
    δ pc (AssertEQ (sexp_of_func left f1) (sexp_of_func right f2)) ∧
    ∃ pci,
    prod ! pc = Some (Eop (left dst1) Havoc nil pci) ∧
    prod ! pci = Some (Eop (right dst2) (Operation Op.Omove) (left dst1 :: nil) pc')

  | RTL.Ibuiltin ef1 args1 dst1 pc1', RTL.Ibuiltin ef2 args2 dst2 pc2' =>
    ef1 = ef2 ∧
    pc1' = pcL' ∧
    pc2' = pcR' ∧
    RTLperm.allowed_builtin ef1 = true ∧
    Forall2 (match_builtin_args pc) args1 args2 ∧
    match_builtin_dst pc pc' dst1 dst2

  | RTL.Istore _ κ1 addr1 args1 src1 pc1', RTL.Istore _ κ2 addr2 args2 src2 pc2' =>
    κ1 = κ2 ∧
    pc1' = pcL' ∧
    pc2' = pcR' ∧
    δ pc (assert_eq_reg (left src1) (right src2)) ∧
    δ pc (AssertEQ (addr addr1 left args1) (addr addr2 right args2)) ∧
    prod ! pc = Some (Egoto pc')

  | _, _ => False
  end.

Definition match_instructions_two
           (iL: RTL.instruction) (pcL1 pcL2: node)
           (iR: RTL.instruction) (pcR1 pcR2: node)
           (pc pc1 pc2: node) : Prop :=
  match iL, iR with
  | RTL.Icond condL argsL thL elL, RTL.Icond condR argsR thR elR =>
    pcL1 = thL ∧ pcL2 = elL ∧
    pcR1 = thR ∧ pcR2 = elR ∧
    prod ! pc = Some (Ebranch condL (List.map left argsL) pc1 pc2) ∧
    ∃ a, assert_iff (comp condL left argsL) (comp condR right argsR) = Some a ∧
         δ pc a
  | _, _ => False
  end.

Definition right_branch_rel (o i: pc_triple) : Prop :=
  let '(pcL', pcR', pc') := o in
  let '(pcL, pcR, pc) := i in
  pcL' = pcL ∧
  ∃ iR,
    progR ! pcR = Some iR ∧
      match_single_instruction right iR pcR' pc pc'.

Definition right_branch : relation pc_triple :=
  clos_refl_trans _ right_branch_rel.

Lemma relax_right_branch {n x y} :
  iter_rel' n right_branch_rel x y →
  right_branch x y.

Definition left_branch_rel (o i: pc_triple) : Prop :=
  let '(pcL', pcR', pc') := o in
  let '(pcL, pcR, pc) := i in
  pcR' = pcR ∧
  ∃ iL,
    progL ! pcL = Some iL ∧
      match_single_instruction left iL pcL' pc pc'.

Fixpoint left_branch (n: nat) (from to: pc_triple) {struct n} : Prop :=
  match n with
  | S n' => ∃ from', left_branch_rel from' from ∧ left_branch n' from' to
  | O => to = from
  end.

Definition fake_branch (from to: pc_triple) : Prop :=
  let '(pcL, pcR, pc) := from in
  let '(pcL', pcR', pc') := to in
  pcL' = pcL ∧ pcR' = pcR ∧
  pc' = List.hd pc (ppmap_get (pcL, pcR) ppmap) ∧
  prod ! pc = Some (Egoto pc') ∧
  (pc' < pc)%positive.
  
Definition synch_branch_ret from : Prop :=
  let '(pcL, pcR, pc) := from in
  ∃ rL rR,
    progL ! pcL = Some (RTL.Ireturn rL) ∧
    progR ! pcR = Some (RTL.Ireturn rR) ∧
    prod ! pc = Some Estop ∧
    match_return rL rR pc.
  
Definition synch_branch_one from to : Prop :=
  let '(pcL, pcR, pc) := from in
  let '(pcL', pcR', pc') := to in
  ∃ iL iR,
    progL ! pcL = Some iL ∧
    progR ! pcR = Some iR ∧
    match_instructions_one iL pcL' iR pcR' pc pc'.

Definition synch_branch_two from to1 to2 : Prop :=
  let '(pcL, pcR, pc) := from in
  let '(pcL1, pcR1, pc1) := to1 in
  let '(pcL2, pcR2, pc2) := to2 in
  ∃ iL iR,
    progL ! pcL = Some iL ∧
    progR ! pcR = Some iR ∧
    match_instructions_two iL pcL1 pcL2 iR pcR1 pcR2 pc pc1 pc2.

Local Notation "{{ a }}" := (@eq _ a) (only parsing).


Inductive code_product_branch_witness : Type :=
| LS `(pc_triple)
| LB `(nat) `(pc_triple) `(pc_triple)
| FB `(pc_triple)
| SBR
| SB1 `(pc_triple) `(pc_triple)
| SB2 `(pc_triple) `(pc_triple) `(pc_triple) `(pc_triple).

Definition successors_of_witness w : list pc_triple :=
  match w with
  | LS to | LB _ _ to | FB to | SB1 _ to => to :: nil
  | SBR => nil
  | SB2 _ _ to1 to2 => to1 :: to2 :: nil
  end.

Fixpoint set_of_list (m: list pc_triple) : pc_triple → Prop :=
  match m with
  | nil => ∅
  | x :: nil => {{ x }}
  | x :: m' => {{ x }} ∪ set_of_list m'
  end.

Remark set_of_list_in m p :
  p ∈ set_of_list m →
  In p m.

Definition code_product_branch_witness_denote from w : Prop :=
  match w with
  | LS to => left_branch_rel to from
  | LB n rb to => left_branch_rel rb from ∧ iter_rel' n right_branch_rel to rb
  | FB to => fake_branch from to
  | SBR => synch_branch_ret from
  | SB1 rb to => synch_branch_one from rb ∧ right_branch to rb
  | SB2 rb1 rb2 to1 to2 => synch_branch_two from rb1 rb2 ∧ right_branch to1 rb1 ∧ right_branch to2 rb2
  end.


Import String.
Import Errors.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.

Arguments OK {_} _.

Definition bcase (b: bool) := Sumbool.sumbool_of_bool b.

Definition β_dec pcL pcR pc : res [β pcL pcR pc].

Definition δ_dec pc a : res [δ pc a].

Definition get_option {X} (ox: option X) m : res { x | ox = Some x } :=
  match ox with
  | Some x => OK (exist _ x eq_refl)
  | None => Error (msg (m tt))
  end.

Definition match_single_instruction_dec ι i pc :
  res { pc' | match_single_instruction ι i (fst pc') pc (snd pc') }.
refine (
    do j' <- get_option (prod ! pc) (λ _, "MSI: no instruction at " ++ PrintPos.print_pos pc);
    let 'exist j Hj := j' in
    _
  ).

Lemma match_return_dec rL rR pc : res [match_return rL rR pc].

Definition res_of_eq_dec {X: Type} `{EqDec X} (x x': X) m : res [ x = x' ] :=
  match eq_dec x x' with
  | Specif.left EQ => OK (Proof EQ)
  | Specif.right _ => Error (msg m)
  end.

Definition match_builtin_args_dec pc aL aR : res [match_builtin_args pc aL aR] :=
  match aL, aR return res [match_builtin_args pc aL aR] with
  | AST.BA r1, AST.BA r2 => δ_dec pc (assert_eq_reg (left r1) (right r2))
  | AST.BA_int i1, AST.BA_int i2 => res_of_eq_dec i1 i2 "match_builtin_args_dec: int mismatch"
  | AST.BA_addrglobal s1 o1, AST.BA_addrglobal s2 o2 =>
    do Hs <- res_of_eq_dec s1 s2 "match_builtin_args_dec: symbol mismatch";
    do Ho <- res_of_eq_dec o1 o2 "match_builtin_args_dec: offset mismatch";
    OK (Proof (conj (proof_of_proof Hs) (proof_of_proof Ho)))
  | _, _ => Error (msg "match_builtin_args_dec: mismatch")
  end.

Definition match_builtin_dst_dec pc dst1 dst2 : res { pc' | match_builtin_dst pc pc' dst1 dst2 } :=
    match dst1, dst2 return res { pc' | match_builtin_dst pc pc' dst1 dst2 } with
    | AST.BR x1, AST.BR x2 =>
      let pci := Pos.succ pc in
      let pc' := Pos.succ pci in
      do Hhavoc' <- res_of_eq_dec (prod ! pc) (Some (Eop (left x1) Havoc nil pci))
         "match_builtin_dst: no havoc";
      do Hmove' <- res_of_eq_dec (prod ! pci) (Some (Eop (right x2) (Operation Op.Omove) (left x1 :: nil) pc'))
         "match_builtin_dst: no move";
      OK (exist _ pc' (ex_intro _ pci (conj (proof_of_proof Hhavoc') (proof_of_proof Hmove'))))
    | AST.BR_none, AST.BR_none =>
      do He'' <- get_option (prod ! pc) (λ _, "match_builtin_dst: no instruction at pc");
      let 'exist e He' := He'' in
      match e return prod ! pc = Some e → res _ with
      | Egoto pc' => λ He, OK (exist _ pc' He)
      | _ => λ _, Error (msg "match_builtin_dst: wrong instruction")
      end He'
    | _, _ => Error (msg "match_builtin_dst: mismatch")
    end.


Fixpoint forall2_dec {X Y: Type} {P: X → Y → Prop} (P_dec: ∀ x y, res [P x y]) (mx: list X) {struct mx} :
  ∀ (my: list Y), res [Forall2 P mx my].

Fixpoint right_branch_validate (entry: pc_triple) (fuel: nat) {struct fuel} : res (pc_triple * nat) :=
  match fuel with
  | O => Error (msg "right_branch_validate: fuel")
  | S fuel' =>
    let '(pcL, pcR, pc) := entry in
    do iR' <- get_option (progR ! pcR) (λ _, "CPV: no right instruction at " ++ PrintPos.print_pos pcR);
    let 'exist iR EQiR := iR' in
    match match_single_instruction_dec right iR pc with
    | OK Hmsi' =>
      let 'exist pc' Hmsi := Hmsi' in
      match β_dec pcL (fst pc') (snd pc') with
      | OK _ =>
        do (e, n) <- right_branch_validate (pcL, fst pc', snd pc') fuel';
        OK (e, S n)
      | Error _ => OK (entry, O)
      end
    | Error _ => OK (entry, O)
    end
  end.

Lemma right_branch_validate_sound entry fuel r :
  right_branch_validate entry fuel = OK r →
  iter_rel' (snd r) right_branch_rel (fst r) entry.
Opaque right_branch_validate.

Definition right_branch_validate' entry (fuel: nat) : res { r | iter_rel' (snd r) right_branch_rel (fst r) entry } :=
      match right_branch_validate entry fuel as r
      return (∀ r', r = OK r' → iter_rel' (snd r') right_branch_rel (fst r') entry) → _
      with
      | OK exit =>
        λ H, OK (exist _ exit (H _ eq_refl))
      | Error e => λ _, Error e
      end
      (right_branch_validate_sound entry fuel)
.

Definition is_fake_branch entry : option { exit | fake_branch entry exit }.

Definition keys {X: Type} (m: PPPTree.t X) (p: pc_triple) : Prop :=
  PPPTree.get p m ≠ None.

Definition get {X: Type} {m: PPPTree.t X} {p: pc_triple} : p ∈ keys m → X :=
  match PPPTree.get p m as ox return ox ≠ None → X with
  | None => λ H, False_rect X (H eq_refl)
  | Some x => λ _, x
  end.

Definition in_keys {X: Type} (m: PPPTree.t X) (p: pc_triple) : bool :=
  match PPPTree.get p m with
  | None => false | Some _ => true end.

Remark keysP {X: Type} (m: PPPTree.t X) (p: pc_triple) : reflect (keys m p) (in_keys m p).

Record state : Type := PPState {
  worklist: list pc_triple;
  cutpoints: PPPTree.t code_product_branch_witness;
  cutpoints_denote : ∀ ppp w, PPPTree.get ppp cutpoints = Some w → code_product_branch_witness_denote ppp w
}.

Definition with_worklist (wl: list pc_triple) (s: state) : state :=
  {| worklist := wl; cutpoints := cutpoints s; cutpoints_denote := cutpoints_denote s |}.

Definition cutpoints_stable cutpoints : Prop :=
  ∀ ppp w,
    PPPTree.get ppp cutpoints = Some w →
    set_of_list (successors_of_witness w) ⊆ keys cutpoints.

Definition cutpoints_stable_dec cutpoints : res [cutpoints_stable cutpoints].
refine
    match bcase (PPPP.for_all cutpoints
                              (λ _ w, List.forallb (in_keys cutpoints)
                                                   (successors_of_witness w)
                ))
    with
    | Specif.left H => OK (Proof _)
    | Specif.right _ => Error (msg "cutpoints not stable")
    end.

Definition has_right_instruction w : bool :=
  match w with
  | LS _
  | LB O _ _
  | FB _ => false
  | LB (S _) _ _
  | SBR | SB1 _ _ | SB2 _ _ _ _ => true
  end.

Remark has_right_instruction_or_has_a_single_successor w :
  has_right_instruction w = true ∨ List.length (successors_of_witness w) = S O.

Definition get_height heights π : nat :=
  match PPPTree.get π heights with
  | Some h => h
  | None => O
  end.

Definition heights_spec cut_points heights : Prop :=
  ∀ ppp w,
    PPPTree.get ppp cut_points = Some w →
    match get_height heights ppp with
    | O => has_right_instruction w = true
    | S h =>
      has_right_instruction w = false ∧
      ∀ ppp',
        In ppp' (successors_of_witness w) →
        get_height heights ppp' = h
    end.

Definition heights_dec cut_points heights : res [ heights_spec cut_points heights ].
refine
    match bcase (PPPP.for_all cut_points
                              (λ ppp w,
                               match get_height heights ppp with
                               | O => has_right_instruction w
                               | S h =>
                                 if has_right_instruction w
                                 then false else
                                 List.forallb (λ ppp', eq_dec (get_height heights ppp') h) (successors_of_witness w)
                               end))
    with
    | Specif.left H => OK (Proof _)
    | Specif.right _ => Error (msg "cutpoints heights not valid")
    end.

Definition correct_witness_sequence w w' : bool :=
  match w, w' with
  | LS _, (LS _ | LB _ _ _) => true
  | LS _, _ => false
  | LB O _ _, FB _ => false
  | _, _ => true
  end.

Definition correct_witness_sequences cutpoints : Prop :=
  ∀ ppp w,
    PPPTree.get ppp cutpoints = Some w →
    ∀ ppp',
      In ppp' (successors_of_witness w)→
      ∀ w',
        PPPTree.get ppp' cutpoints = Some w' →
        correct_witness_sequence w w' = true.

Definition correct_witness_sequences_dec cutpoints : res [correct_witness_sequences cutpoints].
refine
    match bcase (PPPP.for_all cutpoints
                              (λ _ w, List.forallb (λ ppp',
                                                    match PPPTree.get ppp' cutpoints with
                                                    | None => false
                                                    | Some w' => correct_witness_sequence w w'
                                                    end)
                                                   (successors_of_witness w)
                ))
    with
    | Specif.left H => OK (Proof _)
    | Specif.right _ => Error (msg "cutpoints do not obey the sequence rules")
    end.

Definition initial_state (entry: pc_triple) : state.

Definition add_cutpoint (pc: pc_triple) (w: code_product_branch_witness)
   (W: code_product_branch_witness_denote pc w)
   (s: state) : state.

Definition has_hint pc (s: side) : res [ hints ! pc = Some s ] :=
  res_of_eq_dec (hints ! pc) (Some s) "wrong hint".

Fixpoint async_branch (entry: pc_triple) (s: state) (fuel: nat) {struct fuel}
  : res ({ r | iter_rel' (snd r) right_branch_rel (fst r) entry } + pc_triple * state).

Definition async_branch' entry s fuel :=
  match async_branch entry s fuel with
  | OK (inr (exit, s)) => OK (exit, s)
  | OK (inl _) => Error (msg "async_branch': lone right branch")
  | Error e => Error e
  end.

Fixpoint code_product_validate (s: state) (fuel: nat) {struct fuel}
  : res state.
  refine (
      match fuel with
      | O => Error (msg "code_product_validate: fuel")
      | S fuel' =>
      match worklist s with
      | nil => OK s
      | entry :: worklist' =>

      if in_keys (cutpoints s) entry
      then code_product_validate (with_worklist worklist' s) fuel'
      else

        match is_fake_branch entry with
        | Some (exist exit Hfake) =>
          code_product_validate
            (with_worklist (exit :: worklist')
                           (add_cutpoint entry (FB exit) Hfake s))
            fuel'

        | None =>

        match async_branch' entry s fuel with
        | OK (exit, s) =>
              code_product_validate
                (with_worklist (exit :: worklist') s)
                fuel'

        | Error _ =>

        let '(pcL, pcR, pc) := entry in
        do iL' <- get_option (progL ! pcL) (λ _, "CPV: no left instruction at " ++ PrintPos.print_pos pcL);
        let 'exist iL EQiL := iL' in
        do iR' <- get_option (progR ! pcR) (λ _, "CPV: no right instruction at " ++ PrintPos.print_pos pcR);
        let 'exist iR EQiR := iR' in

        match iL as iL' return iL = iL' → _ with
        | RTL.Ireturn rL =>
          λ iLret,
          match iR as iR' return iR = iR' → _ with
          | RTL.Ireturn rR =>
            λ iRret,
            do Hstop' <- res_of_eq_dec (prod ! pc) (Some Estop) "no stop for return";
            let Hstop := proof_of_proof Hstop' in
            do Hret' <- match_return_dec rL rR pc;
            let Hret := proof_of_proof Hret' in
            code_product_validate
       (with_worklist worklist'
                (add_cutpoint (pcL, pcR, pc) SBR _ s))
       fuel'
            | _ => λ _, Error (msg "unmatched return")
          end eq_refl

        | RTL.Iop op1 args1 dst1 pc1' =>
          λ iLop,
          match iR as iR' return iR = iR' → _ with
          | RTL.Iop op2 args2 dst2 pc2' =>
            λ iRop,
            do Hop' <- res_of_eq_dec op1 op2 "operator mismatch";
            let Hop := proof_of_proof Hop' in
            do Hδa' <- forall2_dec (λ aL aR, δ_dec pc (assert_eq_reg (left aL) (right aR))) args1 args2;
            let Hδa := proof_of_proof Hδa' in
            let pci := Pos.succ pc in
            let pc' := Pos.succ pci in
            do Heop' <- res_of_eq_dec (prod ! pc) (Some (Eop (left dst1) (Operation op1) (List.map left args1) pci))
               "no op for op";
            let Heop := proof_of_proof Heop' in
            do Hmove' <- res_of_eq_dec (prod ! pci) (Some (Eop (right dst2) (Operation Op.Omove) (left dst1 :: nil) pc'))
               "no move after op";
            let Hmove := proof_of_proof Hmove' in
            let rb := (pc1', pc2', pc') in
            do Hrb' <- right_branch_validate' rb fuel;
            let 'exist exit Hrb := Hrb' in
            code_product_validate
              (with_worklist ((fst exit) :: worklist')
                             (add_cutpoint (pcL, pcR, pc) (SB1 rb (fst exit)) _ s))
              fuel'
            | _ => λ _, Error (msg "unmatched (dangerous) op")
          end eq_refl

        | RTL.Iload _ κ1 addr1 args1 dst1 pc1' =>
          λ iLload,
          match iR as iR' return iR = iR' → _ with
          | RTL.Iload _ κ2 addr2 args2 dst2 pc2' =>
            λ iRload,
            do Hκ' <- res_of_eq_dec κ1 κ2 "chunk mismatch in load";
            let Hκ := proof_of_proof Hκ' in
            do Hδ' <- δ_dec pc (AssertEQ (addr addr1 left args1) (addr addr2 right args2));
            let Hδ := proof_of_proof Hδ' in
            let pci := Pos.succ pc in
            let pc' := Pos.succ pci in
            do Hhavoc' <- res_of_eq_dec (prod ! pc) (Some (Eop (left dst1) Havoc nil pci))
               "no havoc for load";
            let Hhavoc := proof_of_proof Hhavoc' in
            do Hmove' <- res_of_eq_dec (prod ! pci) (Some (Eop (right dst2) (Operation Op.Omove) (left dst1 :: nil) pc'))
               "no move after load";
            let Hmove := proof_of_proof Hmove' in
            let rb := (pc1', pc2', pc') in
            do Hrb' <- right_branch_validate' rb fuel;
            let 'exist exit Hrb := Hrb' in
            code_product_validate
              (with_worklist (fst exit :: worklist')
                             (add_cutpoint (pcL, pcR, pc) (SB1 rb (fst exit)) _ s))
              fuel'
            | _ => λ _, Error (msg "unmatched load")
          end eq_refl

        | RTL.Istore _ κ1 addr1 args1 src1 pc1' =>
          λ iLstore,
          match iR as iR' return iR = iR' → _ with
          | RTL.Istore _ κ2 addr2 args2 src2 pc2' =>
            λ iRstore,
            do Hκ' <- res_of_eq_dec κ1 κ2 "chunk mismatch in store";
            let Hκ := proof_of_proof Hκ' in
            do Hδs' <- δ_dec pc (assert_eq_reg (left src1) (right src2));
            let Hδs := proof_of_proof Hδs' in
            do Hδa' <- δ_dec pc (AssertEQ (addr addr1 left args1) (addr addr2 right args2));
            let Hδa := proof_of_proof Hδa' in
            let pc' := Pos.succ pc in
            do Hgoto' <- res_of_eq_dec (prod ! pc) (Some (Egoto pc'))
               "no goto for store";
            let Hgoto := proof_of_proof Hgoto' in
            let rb := (pc1', pc2', pc') in
            do Hrb' <- right_branch_validate' rb fuel;
            let 'exist exit Hrb := Hrb' in
            code_product_validate
              (with_worklist (fst exit :: worklist')
                             (add_cutpoint (pcL, pcR, pc) (SB1 rb (fst exit)) _ s))
              fuel'
            | _ => λ _, Error (msg "unmatched store")
          end eq_refl

        | RTL.Icall sg1 f1 args1 dst1 pc1' =>
          λ iLcall,
          match iR as iR' return iR = iR' → _ with
          | RTL.Icall sg2 f2 args2 dst2 pc2' =>
            λ iRcall,
            do Hsg' <- res_of_eq_dec sg1 sg2 "signature mismatch";
            let Hsg := proof_of_proof Hsg' in
            do Hδf' <- δ_dec pc (AssertEQ (sexp_of_func left f1) (sexp_of_func right f2));
            let Hδf := proof_of_proof Hδf' in
            do Hδa' <- forall2_dec (λ aL aR, δ_dec pc (assert_eq_reg (left aL) (right aR))) args1 args2;
            let Hδa := proof_of_proof Hδa' in
            let pci := Pos.succ pc in
            let pc' := Pos.succ pci in
            do Hhavoc' <- res_of_eq_dec (prod ! pc) (Some (Eop (left dst1) Havoc nil pci))
               "no havoc for call";
            let Hhavoc := proof_of_proof Hhavoc' in
            do Hmove' <- res_of_eq_dec (prod ! pci) (Some (Eop (right dst2) (Operation Op.Omove) (left dst1 :: nil) pc'))
               "no move after call";
            let Hmove := proof_of_proof Hmove' in
            let rb := (pc1', pc2', pc') in
            do Hrb' <- right_branch_validate' rb fuel;
            let 'exist exit Hrb := Hrb' in
            code_product_validate
              (with_worklist (fst exit :: worklist')
                             (add_cutpoint (pcL, pcR, pc) (SB1 rb (fst exit)) _ s))
              fuel'
            | _ => λ _, Error (msg "unmatched call")
          end eq_refl

        | RTL.Icond condL argsL thL elL =>
          λ iLcond,
          match iR as iR' return iR = iR' → _ with
          | RTL.Icond condR argsR thR elR =>
            λ iRcond,
            do Hi' <- get_option (prod ! pc) (λ _, "CPV: no instruction at " ++ PrintPos.print_pos pc);
            let 'exist i Hi'' := Hi' in
            match i return prod ! pc = Some i → _ with
            | Ebranch cond args th el =>
              λ Hi,
              do Hcond' <- res_of_eq_dec cond condL
                 "conditions do not match";
            let Hcond := proof_of_proof Hcond' in
            do Hargs' <- res_of_eq_dec args (map left argsL)
               "arguments do not match in condition";
            let Hargs := proof_of_proof Hargs' in
            do Ha' <- get_option (assert_iff (comp condL left argsL) (comp condR right argsR))
               (λ _, "CPV: assert_iff failed in cond");
            let 'exist a Ha := Ha' in
            do Hδa' <- δ_dec pc a;
            let Hδa := proof_of_proof Hδa' in
            let rb1 := (thL, thR, th) in
            do Hrb1' <- right_branch_validate' rb1 fuel;
            let 'exist exit1 Hrb1 := Hrb1' in
            let rb2 := (elL, elR, el) in
            do Hrb2' <- right_branch_validate' rb2 fuel;
            let 'exist exit2 Hrb2 := Hrb2' in
            code_product_validate
              (with_worklist (fst exit1 :: fst exit2 :: worklist')
                             (add_cutpoint (pcL, pcR, pc) (SB2 rb1 rb2 (fst exit1) (fst exit2)) _ s))
              fuel'
            | _ => λ _, Error (msg "no branch for cond")
            end Hi''
          | _ => λ _, Error (msg "unmatched cond")
          end eq_refl

        | RTL.Ibuiltin ef1 args1 dst1 pc1' =>
          λ iLbuiltin,
          match iR as iR' return iR = iR' → _ with
          | RTL.Ibuiltin ef2 args2 dst2 pc2' =>
            λ iRbuiltin,
            do Hef' <- res_of_eq_dec ef1 ef2
               "external functions do not match in builtin";
            let Hef := proof_of_proof Hef' in
            do Hal' <- res_of_eq_dec (RTLperm.allowed_builtin ef1) true
               "builtin is not allowed";
            let Hal := proof_of_proof Hal' in
            do Hargs' <- forall2_dec (match_builtin_args_dec pc) args1 args2;
            let Hargs := proof_of_proof Hargs' in
            do Hdst' <- match_builtin_dst_dec pc dst1 dst2;
            let 'exist pc' Hdst := Hdst' in
            let rb := (pc1', pc2', pc') in
            do Hrb' <- right_branch_validate' rb fuel;
            let 'exist exit Hrb := Hrb' in
            code_product_validate
              (with_worklist (fst exit :: worklist')
                           (add_cutpoint (pcL, pcR, pc) (SB1 rb (fst exit)) _ s))
              fuel'
          | _ => λ _, Error (msg "unmatched builtin")
          end eq_refl

        | _ => λ _, Error (msg ("TODO: " ++ str_of_i iL))
        end eq_refl
        end
        end
      end
      end
    ).

  - clear code_product_validate; abstract (split; [ exists iL, iR; subst iL iR; repeat split; eauto | exact (relax_right_branch Hrb) ]).
  - clear code_product_validate; abstract (split; [ exists iL, iR; subst iL iR; repeat split; eauto | exact (relax_right_branch Hrb) ]).
  - clear code_product_validate; abstract (split; [ exists iL, iR; subst iL iR; repeat split; eauto | exact (relax_right_branch Hrb) ]).
  - clear code_product_validate; abstract (split; [ exists iL, iR; subst iL iR; repeat split; eauto | exact (relax_right_branch Hrb) ]).
  - clear code_product_validate; abstract (split; [ exists iL, iR; subst iL iR; repeat split; eauto | exact (relax_right_branch Hrb) ]).
  - clear code_product_validate; abstract (split; [ exists iL, iR; subst iL iR; repeat split | split; eauto using relax_right_branch ]; eauto; congruence).
  - clear code_product_validate; abstract (subst iL iR; vauto).
  Defined.