proposition: Lemma valid_check_bbZextend pos lres : C.valid rho (check_bbZextend pos lres).
proof: Proof. unfold check_bbZextend. case_eq (S.get s pos); [intros _|intros l1 [ |l] Heq1]; try now apply C.interp_true. case_eq (Lit.is_pos l1); intro Heq2; simpl; try now apply C.interp_true. case_eq (Lit.is_pos lres); intro Heq3; simpl; try now apply C.interp_true. case_eq (t_form .[ Lit.blit l1]); try (intros; now apply C.interp_true). intros a1 bs1 Heq4. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq5. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | | | | | ] a1' Heq6; try (intros; now apply C.interp_true). - case_eq ((a1 =? a1')); simpl; intros Heq7; try (now apply C.interp_true). case_eq ( check_zextend bs1 bsres i && (N.of_nat (Datatypes.length bs1) =? n)%N ); simpl; intros Heq8; try (now apply C.interp_true). unfold C.valid. simpl. rewrite orb_false_r. unfold Lit.interp. rewrite Heq3. unfold Var.interp. rewrite wf_interp_form; trivial. rewrite Heq5. 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 Heq6. easy. } specialize (@H0 H1). rewrite Heq6 in H0. simpl in H0. rewrite !andb_true_iff in 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 H3 in H0; try (now contradict H0). rename H0 into Hv. generalize (Hs pos). intros HSp. unfold C.valid in HSp. rewrite Heq1 in HSp. unfold C.interp in HSp. unfold existsb in HSp. rewrite orb_false_r in HSp. unfold Lit.interp in HSp. rewrite Heq2 in HSp. unfold Var.interp in HSp. rewrite rho_interp in HSp. rewrite Heq4 in HSp. simpl in HSp. apply BITVECTOR_LIST.bv_eq_reflect in HSp. unfold get_type' in H2. unfold v_type in H2. case_eq (t_interp .[ a1']). intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H2. rewrite Atom.t_interp_wf in Htia1; trivial. unfold apply_binop. apply Typ.eqb_spec in H2. rewrite eqb_spec in Heq7; rewrite Heq7 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 H0. rewrite Heq6. simpl. unfold interp_bv. unfold apply_unop. rewrite !Atom.t_interp_wf; trivial. revert v_vala1 Htia1. rewrite H2. intros v_vala1 Htia1. rewrite Htia1. rewrite !Typ.cast_refl. unfold Bval. assert (H100: (N.of_nat (Datatypes.length (map (Lit.interp rho) bsres))) = (i + n)%N). { rewrite andb_true_iff in Heq8. destruct Heq8 as (Heq8a, Heq8b). rewrite map_length. specialize (@zextend_interp_main bs1 bsres n i). intros. apply H4 in Heq8a. unfold RAWBITVECTOR_LIST.bv_zextn in Heq8a. assert (length (RAWBITVECTOR_LIST.zextend (map (Lit.interp rho) bs1) (N.to_nat i)) = length (map (Lit.interp rho) bsres)). { now rewrite Heq8a. } rewrite RAWBITVECTOR_LIST.length_zextend, !map_length in H5. apply (f_equal (N.of_nat)) in H5. rewrite <- H5. rewrite N.eqb_eq in Heq8b. apply (f_equal (N.to_nat)) in Heq8b. rewrite Nat2N.id in Heq8b. rewrite Heq8b. lia. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bsres)). rewrite H100. rewrite Typ.cast_refl. intros. simpl. 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 H4 in HSp. unfold interp_bv in HSp. rewrite Htia1 in HSp. unfold interp_bv in HSp. revert HSp. assert (H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = n). { rewrite andb_true_iff in Heq8. destruct Heq8 as (Heq8a, Heq8b). rewrite map_length. now rewrite N.eqb_eq in Heq8b. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1)). rewrite H101. rewrite Typ.cast_refl. intros. simpl. rewrite HSp. simpl. unfold BITVECTOR_LIST.bv_zextn. apply eq_rec. simpl. rewrite andb_true_iff in Heq8. destruct Heq8 as (Heq8a, Heq8b). now apply zextend_interp_main. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance