proposition: Lemma valid_check_bbMult pos1 pos2 lres : C.valid rho (check_bbMult pos1 pos2 lres).
proof: Proof. unfold check_bbMult. case_eq (S.get s pos1); [intros _|intros l1 [ |l] Heq1]; try now apply C.interp_true. case_eq (S.get s pos2); [intros _|intros l2 [ |l] Heq2]; try now apply C.interp_true. case_eq (Lit.is_pos l1); intro Heq3; simpl; try now apply C.interp_true. case_eq (Lit.is_pos l2); intro Heq4; simpl; try now apply C.interp_true. case_eq (Lit.is_pos lres); intro Heq5; simpl; try now apply C.interp_true. case_eq (t_form .[ Lit.blit l1]); try (intros; now apply C.interp_true). intros a1 bs1 Heq6. case_eq (t_form .[ Lit.blit l2]); try (intros; now apply C.interp_true). intros a2 bs2 Heq7. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). - case_eq ((a1 =? a1') && (a2 =? a2') ); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( check_mult bs1 bs2 bsres && (N.of_nat (Datatypes.length bs1) =? N)%N ); simpl; intros Heq11; try (now apply C.interp_true). unfold C.valid. simpl. rewrite orb_false_r. unfold Lit.interp. rewrite Heq5. unfold Var.interp. rewrite wf_interp_form; trivial. rewrite Heq8. simpl. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. pose proof (H a). assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. destruct H0. unfold get_type' in H0. unfold v_type in H0. case_eq (t_interp .[ a]). intros v_typea v_vala Htia. rewrite Htia in H0. case_eq (v_typea); intros; rewrite H4 in H0; try (now contradict H0). rename H4 into Hv. generalize (Hs pos1). intros HSp1. unfold C.valid in HSp1. rewrite Heq1 in HSp1. unfold C.interp in HSp1. unfold existsb in HSp1. rewrite orb_false_r in HSp1. unfold Lit.interp in HSp1. rewrite Heq3 in HSp1. unfold Var.interp in HSp1. rewrite rho_interp in HSp1. rewrite Heq6 in HSp1. simpl in HSp1. generalize (Hs pos2). intro HSp2. unfold C.valid in HSp2. rewrite Heq2 in HSp2. unfold C.interp in HSp2. unfold existsb in HSp2. rewrite orb_false_r in HSp2. unfold Lit.interp in HSp2. rewrite Heq4 in HSp2. unfold Var.interp in HSp2. rewrite rho_interp in HSp2. rewrite Heq7 in HSp2. simpl in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. unfold get_type' in H2, H3. unfold v_type in H2, H3. case_eq (t_interp .[ a1']). intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H3. case_eq (t_interp .[ a2']). intros v_typea2 v_vala2 Htia2. rewrite Htia2 in H2. rewrite Atom.t_interp_wf in Htia1; trivial. rewrite Atom.t_interp_wf in Htia2; trivial. unfold apply_binop. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. rewrite andb_true_iff in Heq10. destruct Heq10 as (Heq10a1 & Heq10a2); rewrite eqb_spec in Heq10a1, Heq10a2; rewrite Heq10a1, Heq10a2 in *. assert (interp_form_hatom_bv a = interp_bv t_i (interp_atom (t_atom .[a]))). { rewrite !Atom.t_interp_wf in Htia; trivial. rewrite Htia. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia. easy. } rewrite H4. rewrite Heq9. simpl. unfold interp_bv. unfold apply_binop. rewrite !Atom.t_interp_wf; trivial. revert v_vala1 Htia1. rewrite H3. revert v_vala2 Htia2. rewrite H2. intros v_vala2 Htia2 v_vala1 Htia1. rewrite Htia1, Htia2. rewrite Typ.cast_refl. unfold Bval. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. assert (H100: (N.of_nat (Datatypes.length (map (Lit.interp rho) bsres))) = N). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). pose proof Heq11 as Heq11'. apply prop_main in Heq11. rewrite <- Heq11. rewrite !map_length. specialize (@check_bvmult_length bs1 bs2). intros. simpl in H5. rewrite <- H5. now rewrite N.eqb_eq in Heq11r. now apply check_bvmult_length2 in Heq11'. } generalize (BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bsres)). rewrite H100. rewrite Typ.cast_refl. intros. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { rewrite !Atom.t_interp_wf in Htia; trivial. rewrite Htia1. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia1. easy. } rewrite H5 in HSp1. unfold interp_bv in HSp1. rewrite Htia1 in HSp1. unfold interp_bv in HSp1. revert HSp1. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. assert (H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = N). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. now rewrite map_length. } generalize (BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1)). rewrite H101. rewrite Typ.cast_refl. intros. rewrite HSp1. assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { rewrite !Atom.t_interp_wf in Htia; trivial. rewrite Htia2. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia2. easy. } rewrite H6 in HSp2. unfold interp_bv in HSp2. rewrite Htia2 in HSp2. unfold interp_bv in HSp2. revert HSp2. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. assert (H102: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs2))) = N). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. apply check_bvmult_length2 in Heq11. rewrite Heq11 in Heq11r. now rewrite map_length. } generalize (BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs2)). rewrite H102. rewrite Typ.cast_refl. intros. rewrite HSp2. pose proof Heq11. unfold BITVECTOR_LIST.bv_mult. unfold RAWBITVECTOR_LIST.bv_mult. unfold RAWBITVECTOR_LIST.size, RAWBITVECTOR_LIST.bits. unfold BITVECTOR_LIST.of_bits. unfold BITVECTOR_LIST.bv. unfold RAWBITVECTOR_LIST.of_bits. apply eq_rec. simpl. rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11 & Heq11r). rewrite N.eqb_eq in Heq11r. rewrite map_length, Heq11r. apply check_bvmult_length2 in Heq11. rewrite Heq11 in Heq11r. rewrite map_length, Heq11r. rewrite N.eqb_compare, N.compare_refl. unfold RAWBITVECTOR_LIST.mult_list. rewrite <- prop_bblast_bvmult. rewrite andb_true_iff in H7. destruct H7 as (H7 & H7r). rewrite map_length. apply prop_main in H7. rewrite map_length in H7. rewrite <- H7. easy. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance