diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-29 10:04:11 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-29 10:04:11 +0100 |
commit | af0f6f7689fa3520290a4e2ee8d8ea72786f8150 (patch) | |
tree | d6cde08cc303623edad2a7033a78c44c46e806b6 /src | |
parent | 4c475a386caeaee3e3ef7682840c738cecdee941 (diff) | |
parent | 0c360ec297c42d73c1090958d061447c2bfbe31b (diff) | |
download | vericert-kvx-af0f6f7689fa3520290a4e2ee8d8ea72786f8150.tar.gz vericert-kvx-af0f6f7689fa3520290a4e2ee8d8ea72786f8150.zip |
Merge branch 'develop' into dev-nadesh
Diffstat (limited to 'src')
-rw-r--r-- | src/common/Coquplib.v | 92 | ||||
-rw-r--r-- | src/common/IntegerExtra.v | 266 | ||||
-rw-r--r-- | src/translation/HTLgen.v | 129 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 1767 | ||||
-rw-r--r-- | src/translation/HTLgenspec.v | 116 | ||||
-rw-r--r-- | src/translation/Veriloggen.v | 9 | ||||
-rw-r--r-- | src/translation/Veriloggenproof.v | 58 | ||||
-rw-r--r-- | src/verilog/Array.v | 324 | ||||
-rw-r--r-- | src/verilog/HTL.v | 32 | ||||
-rw-r--r-- | src/verilog/Value.v | 41 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 84 |
11 files changed, 2675 insertions, 243 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 47360d6..5de1e7c 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -28,6 +28,7 @@ From coqup Require Import Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) From compcert.lib Require Export Coqlib. +From compcert Require Integers. Ltac unfold_rec c := unfold c; fold c. @@ -41,6 +42,91 @@ Ltac solve_by_inverts n := Ltac solve_by_invert := solve_by_inverts 1. +Ltac invert x := inversion x; subst; clear x. + +Ltac clear_obvious := + repeat match goal with + | [ H : ex _ |- _ ] => invert H + | [ H : ?C _ = ?C _ |- _ ] => invert H + | [ H : _ /\ _ |- _ ] => invert H + end. + +Ltac kill_bools := + repeat match goal with + | [ H : _ && _ = true |- _ ] => apply andb_prop in H + | [ H : _ || _ = false |- _ ] => apply orb_false_elim in H + + | [ H : _ <=? _ = true |- _ ] => apply Z.leb_le in H + | [ H : _ <=? _ = false |- _ ] => apply Z.leb_gt in H + | [ H : _ <? _ = true |- _ ] => apply Z.ltb_lt in H + | [ H : _ <? _ = false |- _ ] => apply Z.ltb_ge in H + | [ H : _ >=? _ = _ |- _ ] => rewrite Z.geb_leb in H + | [ H : _ >? _ = _ |- _ ] => rewrite Z.gtb_ltb in H + + | [ H : _ =? _ = true |- _ ] => apply Z.eqb_eq in H + | [ H : _ =? _ = false |- _ ] => apply Z.eqb_neq in H + end. + +Ltac unfold_constants := + repeat match goal with + | [ |- context[Integers.Ptrofs.modulus] ] => + replace Integers.Ptrofs.modulus with 4294967296 by reflexivity + | [ H : context[Integers.Ptrofs.modulus] |- _ ] => + replace Integers.Ptrofs.modulus with 4294967296 in H by reflexivity + + | [ |- context[Integers.Ptrofs.min_signed] ] => + replace Integers.Ptrofs.min_signed with (-2147483648) by reflexivity + | [ H : context[Integers.Ptrofs.min_signed] |- _ ] => + replace Integers.Ptrofs.min_signed with (-2147483648) in H by reflexivity + + | [ |- context[Integers.Ptrofs.max_signed] ] => + replace Integers.Ptrofs.max_signed with 2147483647 by reflexivity + | [ H : context[Integers.Ptrofs.max_signed] |- _ ] => + replace Integers.Ptrofs.max_signed with 2147483647 in H by reflexivity + + | [ |- context[Integers.Ptrofs.max_unsigned] ] => + replace Integers.Ptrofs.max_unsigned with 4294967295 by reflexivity + | [ H : context[Integers.Ptrofs.max_unsigned] |- _ ] => + replace Integers.Ptrofs.max_unsigned with 4294967295 in H by reflexivity + + | [ |- context[Integers.Int.modulus] ] => + replace Integers.Int.modulus with 4294967296 by reflexivity + | [ H : context[Integers.Int.modulus] |- _ ] => + replace Integers.Int.modulus with 4294967296 in H by reflexivity + + | [ |- context[Integers.Int.min_signed] ] => + replace Integers.Int.min_signed with (-2147483648) by reflexivity + | [ H : context[Integers.Int.min_signed] |- _ ] => + replace Integers.Int.min_signed with (-2147483648) in H by reflexivity + + | [ |- context[Integers.Int.max_signed] ] => + replace Integers.Int.max_signed with 2147483647 by reflexivity + | [ H : context[Integers.Int.max_signed] |- _ ] => + replace Integers.Int.max_signed with 2147483647 in H by reflexivity + + | [ |- context[Integers.Int.max_unsigned] ] => + replace Integers.Int.max_unsigned with 4294967295 by reflexivity + | [ H : context[Integers.Int.max_unsigned] |- _ ] => + replace Integers.Int.max_unsigned with 4294967295 in H by reflexivity + + | [ |- context[Integers.Ptrofs.unsigned (Integers.Ptrofs.repr ?x) ] ] => + match (eval compute in (0 <=? x)) with + | true => replace (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr x)) + with x by reflexivity + | false => idtac + end + end. + +Ltac simplify := unfold_constants; simpl in *; + repeat (clear_obvious; kill_bools); + simpl in *; try discriminate. + +Global Opaque Nat.div. +Global Opaque Z.mul. + +Infix "==nat" := eq_nat_dec (no associativity, at level 50). +Infix "==Z" := Z.eq_dec (no associativity, at level 50). + (* Definition const (A B : Type) (a : A) (b : B) : A := a. Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *) @@ -71,6 +157,12 @@ Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := | _ => None end. +Definition join {A : Type} (a : option (option A)) : option A := + match a with + | None => None + | Some a' => a' + end. + Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v new file mode 100644 index 0000000..8df70d9 --- /dev/null +++ b/src/common/IntegerExtra.v @@ -0,0 +1,266 @@ +Require Import BinInt. +Require Import Lia. +Require Import ZBinary. + +From bbv Require Import ZLib. +From compcert Require Import Integers Coqlib. + +Require Import Coquplib. + +Local Open Scope Z_scope. + +Module PtrofsExtra. + + Ltac ptrofs_mod_match m := + match goal with + | [ H : ?x = 0 |- context[?x] ] => rewrite H + | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r + | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l + | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r + | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l + | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r + | [ _ : _ |- context[?m mod ?m] ] => + rewrite Z_mod_same_full with (a := m) + | [ _ : _ |- context[0 mod _] ] => + rewrite Z.mod_0_l + | [ _ : _ |- context[(_ mod ?m) mod ?m] ] => + rewrite Zmod_mod + | [ _ : _ |- context[(_ mod Ptrofs.modulus) mod m ] ] => + rewrite <- Zmod_div_mod; + try (simplify; lia || assumption) + + | [ _ : _ |- context[Ptrofs.modulus mod m] ] => + rewrite Zdivide_mod with (a := Ptrofs.modulus); + try (lia || assumption) + + | [ _ : _ |- context[Ptrofs.signed ?a mod Ptrofs.modulus] ] => + rewrite Z.mod_small with (a := Ptrofs.signed a) (b := Ptrofs.modulus) + + | [ _ : _ |- context[(?x - ?y) mod ?m] ] => + rewrite Zminus_mod with (a := x) (b := y) (n := m) + + | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] => + rewrite Zplus_mod with (a := x) (b := y) (n := m) + | [ _ : _ |- context[(?x + ?y) mod ?m] ] => + rewrite Zplus_mod with (a := x) (b := y) (n := m) + + | [ _ : _ |- context[(?x * ?y) mod ?m] ] => + rewrite Zmult_mod with (a := x) (b := y) (n := m) + end. + + Ltac ptrofs_mod_tac m := + repeat (ptrofs_mod_match m); lia. + + Lemma signed_mod_unsigned_mod : + forall x m, + 0 < m -> + Ptrofs.modulus mod m = 0 -> + Ptrofs.signed x mod m = 0 -> + Ptrofs.unsigned x mod m = 0. + Proof. + intros. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed + end; try (simplify; lia); ptrofs_mod_tac m. + Qed. + + Lemma of_int_mod : + forall x m, + Int.signed x mod m = 0 -> + Ptrofs.signed (Ptrofs.of_int x) mod m = 0. + Proof. + intros. + pose proof (Integers.Ptrofs.agree32_of_int eq_refl x) as A. + pose proof Ptrofs.agree32_signed. + apply H0 in A; try reflexivity. + rewrite A. assumption. + Qed. + + Lemma mul_mod : + forall x y m, + 0 < m -> + (m | Ptrofs.modulus) -> + Ptrofs.signed x mod m = 0 -> + Ptrofs.signed y mod m = 0 -> + (Ptrofs.signed (Ptrofs.mul x y)) mod m = 0. + Proof. + intros. unfold Ptrofs.mul. + rewrite Ptrofs.signed_repr_eq. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed + end; try (simplify; lia); ptrofs_mod_tac m. + Qed. + + Lemma add_mod : + forall x y m, + 0 < m -> + (m | Ptrofs.modulus) -> + Ptrofs.signed x mod m = 0 -> + Ptrofs.signed y mod m = 0 -> + (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0. + Proof. + intros. unfold Ptrofs.add. + rewrite Ptrofs.unsigned_repr_eq. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed + end; try (simplify; lia); ptrofs_mod_tac m. + Qed. + + Lemma mul_divu : + forall x y, + 0 < Ptrofs.unsigned x -> + Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 -> + (Integers.Ptrofs.mul x (Integers.Ptrofs.divu y x)) = y. + Proof. + intros. + + assert (x <> Ptrofs.zero). + { intro. + rewrite H1 in H. + replace (Ptrofs.unsigned Ptrofs.zero) with 0 in H by reflexivity. + lia. } + + exploit (Ptrofs.modu_divu_Euclid y x); auto; intros. + unfold Ptrofs.modu in H2. rewrite H0 in H2. + replace (Ptrofs.repr 0) with Ptrofs.zero in H2 by reflexivity. + rewrite Ptrofs.add_zero in H2. + rewrite Ptrofs.mul_commut. + congruence. + Qed. + + Lemma divu_unsigned : + forall x y, + 0 < Ptrofs.unsigned y -> + Ptrofs.unsigned x < Ptrofs.max_unsigned -> + Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y. + Proof. + intros. + unfold Ptrofs.divu. + rewrite Ptrofs.unsigned_repr; auto. + split. + apply Z.div_pos; auto. + apply Ptrofs.unsigned_range. + apply Z.div_le_upper_bound; auto. + eapply Z.le_trans. + apply Z.lt_le_incl. exact H0. + rewrite Z.mul_comm. + apply Z.le_mul_diag_r; simplify; lia. + Qed. + + Lemma mul_unsigned : + forall x y, + Ptrofs.mul x y = + Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y). + Proof. + intros; unfold Ptrofs.mul. + apply Ptrofs.eqm_samerepr. + apply Ptrofs.eqm_mult; exists 0; lia. + Qed. + + Lemma pos_signed_unsigned : + forall x, + 0 <= Ptrofs.signed x -> + Ptrofs.signed x = Ptrofs.unsigned x. + Proof. + intros. + rewrite Ptrofs.unsigned_signed. + destruct (Ptrofs.lt x Ptrofs.zero) eqn:EQ. + unfold Ptrofs.lt in EQ. + destruct (zlt (Ptrofs.signed x) (Ptrofs.signed Ptrofs.zero)); try discriminate. + replace (Ptrofs.signed (Ptrofs.zero)) with 0 in l by reflexivity. lia. + reflexivity. + Qed. +End PtrofsExtra. + +Module IntExtra. + + Ltac int_mod_match m := + match goal with + | [ H : ?x = 0 |- context[?x] ] => rewrite H + | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r + | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l + | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r + | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l + | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r + | [ _ : _ |- context[?m mod ?m] ] => + rewrite Z_mod_same_full with (a := m) + | [ _ : _ |- context[0 mod _] ] => + rewrite Z.mod_0_l + | [ _ : _ |- context[(_ mod ?m) mod ?m] ] => + rewrite Zmod_mod + | [ _ : _ |- context[(_ mod Int.modulus) mod m ] ] => + rewrite <- Zmod_div_mod; + try (simplify; lia || assumption) + + | [ _ : _ |- context[Int.modulus mod m] ] => + rewrite Zdivide_mod with (a := Int.modulus); + try (lia || assumption) + + | [ _ : _ |- context[Int.signed ?a mod Int.modulus] ] => + rewrite Z.mod_small with (a := Int.signed a) (b := Int.modulus) + + | [ _ : _ |- context[(?x - ?y) mod ?m] ] => + rewrite Zminus_mod with (a := x) (b := y) (n := m) + + | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] => + rewrite Zplus_mod with (a := x) (b := y) (n := m) + | [ _ : _ |- context[(?x + ?y) mod ?m] ] => + rewrite Zplus_mod with (a := x) (b := y) (n := m) + + | [ _ : _ |- context[(?x * ?y) mod ?m] ] => + rewrite Zmult_mod with (a := x) (b := y) (n := m) + end. + + Ltac int_mod_tac m := + repeat (int_mod_match m); lia. + + Lemma mul_mod : + forall x y m, + 0 < m -> + (m | Int.modulus) -> + Int.signed x mod m = 0 -> + Int.signed y mod m = 0 -> + (Int.signed (Int.mul x y)) mod m = 0. + Proof. + intros. unfold Int.mul. + rewrite Int.signed_repr_eq. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Int.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed + end; try (simplify; lia); int_mod_tac m. + Qed. + + Lemma add_mod : + forall x y m, + 0 < m -> + (m | Int.modulus) -> + Int.signed x mod m = 0 -> + Int.signed y mod m = 0 -> + (Int.signed (Int.add x y)) mod m = 0. + Proof. + intros. unfold Int.add. + rewrite Int.signed_repr_eq. + + repeat match goal with + | [ _ : _ |- context[if ?x then _ else _] ] => destruct x + | [ _ : _ |- context[_ mod Int.modulus mod m] ] => + rewrite <- Zmod_div_mod; try lia; try assumption + | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed + end; try (simplify; lia); int_mod_tac m. + Qed. +End IntExtra. diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index c96d4c7..a75ef5c 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -17,7 +17,7 @@ *) From compcert Require Import Maps. -From compcert Require Errors Globalenvs. +From compcert Require Errors Globalenvs Integers. From compcert Require Import AST RTL. From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. @@ -131,7 +131,7 @@ Lemma declare_reg_state_incr : s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). @@ -142,7 +142,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)) @@ -280,19 +280,39 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. +Definition check_address_parameter_signed (p : Z) : bool := + Z.eqb (Z.modulo p 4) 0 + && Z.leb Integers.Ptrofs.min_signed p + && Z.leb p Integers.Ptrofs.max_signed. + +Definition check_address_parameter_unsigned (p : Z) : bool := + Z.eqb (Z.modulo p 4) 0 + && Z.leb p Integers.Ptrofs.max_unsigned. + Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := - match a, args with - | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off) - | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off)) + match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (boplitz Vadd r1 off) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Ascaled scale offset, r1::nil => - ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) - | Op.Aindexed2scaled scale offset, r1::r2::nil => - ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (* Stack arrays/referenced variables *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | Op.Aindexed2 offset, r1::r2::nil => + if (check_address_parameter_signed offset) + then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - ret (Vlit (ZToValue 32 a)) - | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other") + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vlit (ZToValue 32 a)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. (** Translate an instruction to a statement. FIX mulhs mulhu *) @@ -374,24 +394,24 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (args : list reg) (stack : reg) : mon expr := - match addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Op.Aindexed off, r1::nil => (* FIXME: Cannot guarantee alignment *) - ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4))))) - | Op.Ascaled scale offset, r1::nil => - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) - then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4))))) - else error (Errors.msg "Htlgen: translate_arr_access address misaligned") - | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Mint32, Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 32 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address misaligned") + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vvari stack - (Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4)))) - (boplitz Vmul r2 (scale / 4)))) - else error (Errors.msg "Htlgen: translate_arr_access address misaligned") - | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) - else error (Errors.msg "Htlgen: eff_addressing misaligned stack offset") - | _, _ => error (Errors.msg "Htlgen: translate_arr_access unsupported addressing") + (Vbinop Vdivu + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (ZToValue 32 4))) + else error (Errors.msg "HTLgen: translate_arr_access address misaligned") + | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) + else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") + | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") end. Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := @@ -418,10 +438,10 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Iload mem addr args dst n' => do src <- translate_arr_access mem addr args stack; do _ <- declare_reg None dst 32; - add_instr n n' (block dst src) + add_instr n n' (nonblock dst src) | Istore mem addr args src n' => do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") @@ -447,7 +467,7 @@ Lemma create_reg_state_incr: s.(st_st) (Pos.succ (st_freshreg s)) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) (st_datapath s) (st_controllogic s)). @@ -459,7 +479,7 @@ Definition create_reg (i : option io) (sz : nat) : mon reg := s.(st_st) (Pos.succ r) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) (st_arrdecls s) (st_datapath s) (st_controllogic s)) @@ -472,27 +492,31 @@ Lemma create_arr_state_incr: (Pos.succ (st_freshreg s)) (st_freshstate s) s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls)) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) (st_datapath s) (st_controllogic s)). Proof. constructor; simpl; auto with htlh. Qed. -Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon reg := +Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := fun s => let r := s.(st_freshreg) in - OK r (mkstate + OK (r, ln) (mkstate s.(st_st) (Pos.succ r) (st_freshstate s) s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls)) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) (st_datapath s) (st_controllogic s)) (create_arr_state_incr s sz ln i). +Definition stack_correct (sz : Z) : bool := + (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). + Definition transf_module (f: function) : mon module := + if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; - do stack <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); + do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); do start <- create_reg (Some Vinput) 1; @@ -506,20 +530,22 @@ Definition transf_module (f: function) : mon module := f.(fn_entrypoint) current_state.(st_st) stack + stack_len fin rtrn start rst clk current_state.(st_scldecls) - current_state.(st_arrdecls)). + current_state.(st_arrdecls)) + else error (Errors.msg "Stack size misalignment."). Definition max_state (f: function) : state := let st := Pos.succ (max_reg_function f) in mkstate st (Pos.succ st) (Pos.succ (max_pc_function f)) - (AssocMap.set st (None, Scalar 32) (st_scldecls (init_state st))) + (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) (st_arrdecls (init_state st)) (st_datapath (init_state st)) (st_controllogic (init_state st)). @@ -529,7 +555,7 @@ Definition transl_module (f : function) : Errors.res module := Definition transl_fundef := transf_partial_fundef transl_module. -Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. +(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *) (*Definition transl_main_fundef f : Errors.res HTL.fundef := match f with @@ -546,11 +572,18 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -(*Definition main_is_internal (p : RTL.program): Prop := +Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in - forall b m, - Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> - Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m). + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal _) => true + | _ => false + end + | _ => false + end. -Definition tranls_program_with_proof (p : RTL.program) : Errors.res { p' : HTL.program | main_is_internal p }. -*) +Definition transl_program (p : RTL.program) : Errors.res HTL.program := + if main_is_internal p + then transform_partial_program transl_fundef p + else Errors.Error (Errors.msg "Main function is not Internal."). diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 9786d23..2f296f2 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -18,9 +18,11 @@ From compcert Require RTL Registers AST Integers. From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap. +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra. From coqup Require HTL Verilog. +Require Import Lia. + Local Open Scope assocmap. Hint Resolve Smallstep.forward_simulation_plus : htlproof. @@ -42,44 +44,71 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) := asa!(m.(HTL.mod_st)) = Some (posToValue 32 st). Hint Unfold state_st_wf : htlproof. -Inductive match_stacks : list RTL.stackframe -> list HTL.stackframe -> Prop := +Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : + Verilog.assocmap_arr -> Prop := +| match_arr : forall asa stack, + asa ! (m.(HTL.mod_stk)) = Some stack /\ + stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ + (forall ptr, + 0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> + opt_val_value_lessdef (Mem.loadv AST.Mint32 mem + (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))) + (Option.default (NToValue 32 0) + (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> + match_arrs m f sp mem asa. + +Definition stack_based (v : Values.val) (sp : Values.block) : Prop := + match v with + | Values.Vptr sp' off => sp' = sp + | _ => True + end. + +Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := + forall r, stack_based (Registers.Regmap.get r rs) sp. + +Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) + (sp : Values.val) : Prop := + forall ptr, + 0 <= ptr < (stack_length / 4) -> + stack_based (Option.default + Values.Vundef + (Mem.loadv AST.Mint32 m + (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) + spb. + +Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop := | match_stacks_nil : - match_stacks nil nil + match_stacks mem nil nil | match_stacks_cons : - forall cs lr r f sp pc rs m assoc + forall cs lr r f sp sp' pc rs m asr asa (TF : tr_module f m) - (ST: match_stacks cs lr) - (MA: match_assocmaps f rs assoc), - match_stacks (RTL.Stackframe r f sp pc rs :: cs) - (HTL.Stackframe r m pc assoc :: lr). - -Inductive match_arrs (m : HTL.module) : RTL.function -> mem -> AssocMap.t (list value) -> Prop := -| match_arr : forall mem asa stack sp f sz, - sz = f.(RTL.fn_stacksize) -> - asa ! (m.(HTL.mod_stk)) = Some stack -> - (forall ptr, - 0 <= ptr < sz -> - nth_error stack (Z.to_nat ptr) = - (Coquplib.Option.bind (Mem.loadv AST.Mint32 mem - (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr))) - valToValue)) -> - match_arrs m f mem asa. + (ST: match_stacks mem cs lr) + (MA: match_assocmaps f rs asr) + (MARR : match_arrs m f sp mem asa) + (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) + (RSBP: reg_stack_based_pointers sp' rs) + (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp), + match_stacks mem (RTL.Stackframe r f sp pc rs :: cs) + (HTL.Stackframe r m pc asr asa :: lr). Inductive match_states : RTL.state -> HTL.state -> Prop := -| match_state : forall asa asr sf f sp rs mem m st res +| match_state : forall asa asr sf f sp sp' rs mem m st res (MASSOC : match_assocmaps f rs asr) (TF : tr_module f m) (WF : state_st_wf m (HTL.State res m st asr asa)) - (MS : match_stacks sf res) - (MA : match_arrs m f mem asa), + (MS : match_stacks mem sf res) + (MARR : match_arrs m f sp mem asa) + (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) + (RSBP: reg_stack_based_pointers sp' rs) + (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp), match_states (RTL.State sf f sp st rs mem) (HTL.State res m st asr asa) | match_returnstate : forall - v v' stack m res - (MS : match_stacks stack res), + v v' stack mem res + (MS : match_stacks mem stack res), val_value_lessdef v v' -> - match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v') + match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v') | match_initial_call : forall f m m0 (TF : tr_module f m), @@ -87,12 +116,23 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ + main_is_internal p = true. + +Definition match_prog_matches : + forall p tp, + match_prog p tp -> + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + Proof. intros. unfold match_prog in H. tauto. Qed. Lemma transf_program_match: forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. Proof. - intros. apply Linking.match_transform_partial_program; auto. + intros. unfold transl_program in H. + destruct (main_is_internal p) eqn:?; try discriminate. + unfold match_prog. split. + apply Linking.match_transform_partial_program; auto. + assumption. Qed. Lemma regs_lessdef_add_greater : @@ -129,6 +169,94 @@ Proof. Qed. Hint Resolve regs_lessdef_add_match : htlproof. +Lemma list_combine_none : + forall n l, + length l = n -> + list_combine Verilog.merge_cell (list_repeat None n) l = l. +Proof. + induction n; intros; simplify. + - symmetry. apply length_zero_iff_nil. auto. + - destruct l; simplify. + rewrite list_repeat_cons. + simplify. f_equal. + eauto. +Qed. + +Lemma combine_none : + forall n a, + a.(arr_length) = n -> + arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. +Proof. + intros. + unfold combine. + simplify. + + rewrite <- (arr_wf a) in H. + apply list_combine_none. + assumption. +Qed. + +Lemma list_combine_lookup_first : + forall l1 l2 n, + length l1 = length l2 -> + nth_error l1 n = Some None -> + nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. +Proof. + induction l1; intros; simplify. + + rewrite nth_error_nil in H0. + discriminate. + + destruct l2 eqn:EQl2. simplify. + simpl in H. invert H. + destruct n; simpl in *. + invert H0. simpl. reflexivity. + eauto. +Qed. + +Lemma combine_lookup_first : + forall a1 a2 n, + a1.(arr_length) = a2.(arr_length) -> + array_get_error n a1 = Some None -> + array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. +Proof. + intros. + + unfold array_get_error in *. + apply list_combine_lookup_first; eauto. + rewrite a1.(arr_wf). rewrite a2.(arr_wf). + assumption. +Qed. + +Lemma list_combine_lookup_second : + forall l1 l2 n x, + length l1 = length l2 -> + nth_error l1 n = Some (Some x) -> + nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). +Proof. + induction l1; intros; simplify; auto. + + destruct l2 eqn:EQl2. simplify. + simpl in H. invert H. + destruct n; simpl in *. + invert H0. simpl. reflexivity. + eauto. +Qed. + +Lemma combine_lookup_second : + forall a1 a2 n x, + a1.(arr_length) = a2.(arr_length) -> + array_get_error n a1 = Some (Some x) -> + array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). +Proof. + intros. + + unfold array_get_error in *. + apply list_combine_lookup_second; eauto. + rewrite a1.(arr_wf). rewrite a2.(arr_wf). + assumption. +Qed. + (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) Lemma assumption_32bit : forall v, @@ -205,13 +333,16 @@ Section CORRECTNESS. Hypothesis TRANSL : match_prog prog tprog. -(* Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Lemma TRANSL' : + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. + Proof. intros; apply match_prog_matches; assumption. Qed. + + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. - Proof - (Genv.find_symbol_transf_partial TRANSL). + Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. Lemma function_ptr_translated: forall (b: Values.block) (f: RTL.fundef), @@ -219,7 +350,7 @@ Section CORRECTNESS. exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. Proof. - intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. + intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. @@ -229,21 +360,21 @@ Section CORRECTNESS. exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. Proof. - intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros. exploit (Genv.find_funct_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. Lemma senv_preserved: Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof - (Genv.senv_transf_partial TRANSL). + (Genv.senv_transf_partial TRANSL'). Hint Resolve senv_preserved : htlproof. Lemma eval_correct : - forall sp op rs args m v v' e asr asa f, + forall sp op rs args m v v' e asr asa f s s' i, Op.eval_operation ge sp op (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> - tr_op op args e -> + translate_instr op args s = OK e s' i -> val_value_lessdef v v' -> Verilog.expr_runp f asr asa e v'. Admitted. @@ -281,6 +412,7 @@ Section CORRECTNESS. exists asr' asa', HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). + Theorem transl_step_correct: forall (S1 : RTL.state) t S2, RTL.step ge S1 t S2 -> @@ -295,23 +427,54 @@ Section CORRECTNESS. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. + apply assumption_32bit. (* processing of state *) econstructor. - simpl. trivial. + simplify. econstructor. econstructor. econstructor. + simplify. - (* prove stval *) - unfold merge_assocmap. - unfold_merge. simpl. apply AssocMap.gss. + unfold Verilog.merge_regs. + unfold_merge. apply AssocMap.gss. (* prove match_state *) rewrite assumption_32bit. - constructor; auto. + econstructor; simplify; eauto. + + unfold Verilog.merge_regs. unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. + unfold Verilog.merge_regs. unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss. + + (* prove match_arrs *) + invert MARR. simplify. + unfold HTL.empty_stack. simplify. unfold Verilog.merge_arrs. + econstructor. + simplify. repeat split. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len; auto. + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + + assumption. + - (* Iop *) (* destruct v eqn:?; *) (* try ( *) @@ -390,11 +553,1317 @@ Section CORRECTNESS. (* assumption. *) admit. - - admit. - - admit. + Ltac rt := + repeat match goal with + | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate + | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => + let EQ1 := fresh "EQ" in + let EQ2 := fresh "EQ" in + destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * + | [ _ : context[if ?x then _ else _] |- _ ] => + let EQ := fresh "EQ" in + destruct x eqn:EQ; simpl in * + | [ H : ret _ _ = _ |- _ ] => invert H + | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x + end. + + - (* FIXME: Should be able to use the spec to avoid destructing here? *) + destruct c, chunk, addr, args; simplify; rt; simplify. + + + (** Preamble *) + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify. + + rewrite ARCHI in H1. simplify. + subst. + + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + apply H6 in HPler0. + invert HPler0; try congruence. + rewrite EQr0 in H8. + invert H8. + clear H0. clear H6. + + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; simplify. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. + + (** Read bounds assumption *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + { rewrite HeqOFFSET. + apply PtrofsExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + rewrite Integers.Ptrofs.signed_repr; try assumption. + admit. (* FIXME: Register bounds. *) + apply PtrofsExtra.of_int_mod. + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + } + + (** Normalisation proof *) + assert (Integers.Ptrofs.repr + (4 * Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + as NORMALISE. + { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. + rewrite <- PtrofsExtra.mul_unsigned. + apply PtrofsExtra.mul_divu; simplify; auto; lia. } + + (** Normalised bounds proof *) + assert (0 <= + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) + < (RTL.fn_stacksize f / 4)) + as NORMALISE_BOUND. + { split. + apply Integers.Ptrofs.unsigned_range_2. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu at 2 in H0. + rewrite H0. clear H0. + rewrite Integers.Ptrofs.unsigned_repr; simplify. + apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; try lia. + split. + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } + + inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; + clear NORMALISE_BOUND. + + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + apply assumption_32bit. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. simplify. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ1]). (* FIXME: These will be shelved and cause sadness. *) + eapply Verilog.erun_Vbinop with (EQ := ?[EQ2]). + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. + f_equal. + + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. + + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. + apply regs_lessdef_add_match. + + (** Equality proof *) + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1)) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + (** States well formed *) + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match arrays *) + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + assumption. + + (** RSBP preservation *) + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r1 dst); try rewrite e. (* FIXME: Prepare this for automation *) + + rewrite Registers.Regmap.gss. + unfold arr_stack_based_pointers in ASBP. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. + simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. + assumption. + simplify. + + rewrite Registers.Regmap.gso; auto. + + + (** Preamble *) + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + pose proof (RSBP r1) as RSBPr1. + + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. + + rewrite ARCHI in H1. simplify. + subst. + clear RSBPr1. + + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + pose proof (H0 r1). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + assert (HPler1 : Ple r1 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H6 in HPler0. + apply H8 in HPler1. + invert HPler0; invert HPler1; try congruence. + rewrite EQr0 in H10. + rewrite EQr1 in H12. + invert H10. invert H12. + clear H0. clear H6. clear H8. + + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; simplify. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) + (Integers.Int.repr z0)))) as OFFSET. + + (** Read bounds assumption *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + { rewrite HeqOFFSET. + apply PtrofsExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + rewrite Integers.Ptrofs.signed_repr; try assumption. + admit. (* FIXME: Register bounds. *) + apply PtrofsExtra.of_int_mod. + apply IntExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + apply IntExtra.mul_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + admit. (* FIXME: Register bounds. *) + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + } + + (** Normalisation proof *) + assert (Integers.Ptrofs.repr + (4 * Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + as NORMALISE. + { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. + rewrite <- PtrofsExtra.mul_unsigned. + apply PtrofsExtra.mul_divu; simplify; auto; lia. } + + (** Normalised bounds proof *) + assert (0 <= + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) + < (RTL.fn_stacksize f / 4)) + as NORMALISE_BOUND. + { split. + apply Integers.Ptrofs.unsigned_range_2. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu at 2 in H0. + rewrite H0. clear H0. + rewrite Integers.Ptrofs.unsigned_repr; simplify. + apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; try lia. + split. + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } + + inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; + clear NORMALISE_BOUND. + + (** Start of proof proper *) + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + apply assumption_32bit. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. simplify. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]). (* FIXME: These will be shelved and cause sadness. *) + eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]). + eapply Verilog.erun_Vbinop with (EQ := ?[EQ5]). + econstructor. econstructor. econstructor. econstructor. + econstructor. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]). + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. + + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. + f_equal. + + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. + + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. + apply regs_lessdef_add_match. + + (** Equality proof *) + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = valueToNat + (vdiv (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5) + (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3)) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + (** States well formed *) + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match arrays *) + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + assumption. + + (** RSBP preservation *) + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r2 dst); try rewrite e. (* FIXME: Prepare this for automation *) + + rewrite Registers.Regmap.gss. + unfold arr_stack_based_pointers in ASBP. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. + simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. + assumption. + simplify. + + rewrite Registers.Regmap.gso; auto. + + + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + rewrite ARCHI in H0. simplify. + + unfold check_address_parameter_unsigned in *; + unfold check_address_parameter_signed in *; simplify. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H1. clear ZERO. + rewrite Integers.Ptrofs.add_zero_l in H1. + + remember i0 as OFFSET. + + (** Read bounds assumption *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (** Modular preservation proof *) + rename H0 into MOD_PRESERVE. + + (** Normalisation proof *) + assert (Integers.Ptrofs.repr + (4 * Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) + as NORMALISE. + { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. + rewrite <- PtrofsExtra.mul_unsigned. + apply PtrofsExtra.mul_divu; simplify; auto; try lia. } + + (** Normalised bounds proof *) + assert (0 <= + Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) + < (RTL.fn_stacksize f / 4)) + as NORMALISE_BOUND. + { split. + apply Integers.Ptrofs.unsigned_range_2. + assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. + unfold Integers.Ptrofs.divu at 2 in H0. + rewrite H0. clear H0. + rewrite Integers.Ptrofs.unsigned_repr; simplify. + apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; try lia. + split. + apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_le_upper_bound; lia. } + + inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; + clear NORMALISE_BOUND. + + (** Start of proof proper *) + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + apply assumption_32bit. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. econstructor. simplify. + + all: simplify. + + (** Verilog array lookup *) + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5. + f_equal. + + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. + + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. + apply regs_lessdef_add_match. + + (** Equality proof *) + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H7. clear ZERO. + setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4)))). + + exploit H7. + rewrite Z2Nat.id; eauto. + apply Z.div_pos; lia. + + intros I. + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) + as EXPR_OK by admit. + rewrite <- EXPR_OK. + rewrite NORMALISE in I. + rewrite H1 in I. + invert I. assumption. + + (** PC match *) + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + (** States well formed *) + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (** Match arrays *) + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + assumption. + + (** RSBP preservation *) + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r0 dst); try rewrite e. (* FIXME: Prepare this for automation *) + + rewrite Registers.Regmap.gss. + unfold arr_stack_based_pointers in ASBP. + specialize (ASBP (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). + exploit ASBP; auto; intros I. + + rewrite NORMALISE in I. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in I. clear ZERO. + simplify. + rewrite Integers.Ptrofs.add_zero_l in I. + rewrite H1 in I. + assumption. + simplify. + + rewrite Registers.Regmap.gso; auto. + + - destruct c, chunk, addr, args; simplify; rt; simplify. + + (** Preamble *) + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify. + + rewrite ARCHI in H1. simplify. + subst. + + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + apply H6 in HPler0. + invert HPler0; try congruence. + rewrite EQr0 in H8. + invert H8. + clear H0. clear H6. + + unfold check_address_parameter_unsigned in *; + unfold check_address_parameter_signed in *; simplify. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. + + (** Read bounds assumption *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH by admit. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + { rewrite HeqOFFSET. + apply PtrofsExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + rewrite Integers.Ptrofs.signed_repr; try assumption. + admit. (* FIXME: Register bounds. *) + apply PtrofsExtra.of_int_mod. + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + } + + (** Start of proof proper *) + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + apply assumption_32bit. + econstructor. econstructor. econstructor. + eapply Verilog.stmnt_runp_Vnonblock_arr. simplify. + econstructor. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]). + eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]). + econstructor. + econstructor. + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + + all: simplify. + + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. + unfold_merge. + apply AssocMap.gss. + + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. + + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. + apply regs_lessdef_add_greater. apply greater_than_max_func. + assumption. + + (** States well formed *) + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. + apply AssocMap.gss. + + (** Match stacks *) + admit. + + (** Equality proof *) + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7)) + as EXPR_OK by admit. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. + + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + rewrite AssocMap.gss. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. simplify. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + rewrite H4. reflexivity. + + intros. + destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). + + erewrite Mem.load_store_same. + 2: { rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite e. + rewrite Integers.Ptrofs.unsigned_repr. + exact H1. + apply Integers.Ptrofs.unsigned_range_2. } + constructor. + erewrite combine_lookup_second. + simpl. + assert (Ple src (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H0 in H14. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H14; eauto. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. auto. + + assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). + rewrite Z.mul_comm in H14. + rewrite Z_div_mult in H14; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H14 by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in H14; unfold_constants; try lia. + rewrite H14. rewrite EXPR_OK. + rewrite array_get_error_set_bound. + reflexivity. + unfold arr_length, arr_repeat. simpl. + rewrite list_repeat_len. lia. + + erewrite Mem.load_store_other with (m1 := m). + 2: { exact H1. } + 2: { right. + rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite Integers.Ptrofs.unsigned_repr. + simpl. + destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. + right. + apply ZExtra.mod_0_bounds; try lia. + apply ZLib.Z_mod_mult'. + invert H13. + rewrite Z2Nat.id in H19; try lia. + apply Zmult_lt_compat_r with (p := 4) in H19; try lia. + rewrite ZLib.div_mul_undo in H19; try lia. + split; try lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + } + + rewrite <- EXPR_OK. + rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). + destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). + apply Z.mul_cancel_r with (p := 4) in e; try lia. + rewrite ZLib.div_mul_undo in e; try lia. + rewrite combine_lookup_first. + eapply H7; eauto. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. auto. + rewrite array_gso. + unfold array_get_error. + unfold arr_repeat. + simplify. + apply list_repeat_lookup. + lia. + unfold_constants. + intro. + apply Z2Nat.inj_iff in H14; try lia. + apply Z.div_pos; try lia. + apply Integers.Ptrofs.unsigned_range. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + unfold arr_stack_based_pointers. + intros. + destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). + + simplify. + erewrite Mem.load_store_same. + 2: { rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite e. + rewrite Integers.Ptrofs.unsigned_repr. + exact H1. + apply Integers.Ptrofs.unsigned_range_2. } + simplify. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. + destruct (Archi.ptr64); try discriminate. + pose proof (RSBP src). rewrite EQ_SRC in H0. + assumption. + + simpl. + erewrite Mem.load_store_other with (m1 := m). + 2: { exact H1. } + 2: { right. + rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite Integers.Ptrofs.unsigned_repr. + simpl. + destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. + right. + apply ZExtra.mod_0_bounds; try lia. + apply ZLib.Z_mod_mult'. + invert H0. + apply Zmult_lt_compat_r with (p := 4) in H14; try lia. + rewrite ZLib.div_mul_undo in H14; try lia. + split; try lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + } + apply ASBP; assumption. + + + (** Preamble *) + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + pose proof (RSBP r1) as RSBPr1. + + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. + + rewrite ARCHI in H1. simplify. + subst. + clear RSBPr1. + + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + pose proof (H0 r1). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + assert (HPler1 : Ple r1 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H6 in HPler0. + apply H8 in HPler1. + invert HPler0; invert HPler1; try congruence. + rewrite EQr0 in H10. + rewrite EQr1 in H12. + invert H10. invert H12. + clear H0. clear H6. clear H8. + + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; simplify. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) + (Integers.Int.repr z0)))) as OFFSET. + + (** Read bounds assumption *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + { rewrite HeqOFFSET. + apply PtrofsExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + rewrite Integers.Ptrofs.signed_repr; try assumption. + admit. (* FIXME: Register bounds. *) + apply PtrofsExtra.of_int_mod. + apply IntExtra.add_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + apply IntExtra.mul_mod; simplify; try lia. + exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) + admit. (* FIXME: Register bounds. *) + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + } + + (** Start of proof proper *) + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + apply assumption_32bit. + econstructor. econstructor. econstructor. + eapply Verilog.stmnt_runp_Vnonblock_arr. simplify. + econstructor. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]). + eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]). + eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]). + econstructor. econstructor. econstructor. econstructor. + econstructor. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]). + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + + all: simplify. + + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. + unfold_merge. + apply AssocMap.gss. + + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. + + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. + apply regs_lessdef_add_greater. apply greater_than_max_func. + assumption. + + (** States well formed *) + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. + apply AssocMap.gss. + + (** Match stacks *) + admit. + + (** Equality proof *) + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (vdiv + (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12) + ?EQ10) (ZToValue 32 4) ?EQ9)) + as EXPR_OK by admit. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. + + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + rewrite AssocMap.gss. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. simplify. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + rewrite H4. reflexivity. + + intros. + destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). + + erewrite Mem.load_store_same. + 2: { rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite e. + rewrite Integers.Ptrofs.unsigned_repr. + exact H1. + apply Integers.Ptrofs.unsigned_range_2. } + constructor. + erewrite combine_lookup_second. + simpl. + assert (Ple src (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H0 in H21. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H21; eauto. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. auto. + + assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). + rewrite Z.mul_comm in H21. + rewrite Z_div_mult in H21; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H21 by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in H21; unfold_constants; try lia. + rewrite H21. rewrite EXPR_OK. + rewrite array_get_error_set_bound. + reflexivity. + unfold arr_length, arr_repeat. simpl. + rewrite list_repeat_len. lia. + + erewrite Mem.load_store_other with (m1 := m). + 2: { exact H1. } + 2: { right. + rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite Integers.Ptrofs.unsigned_repr. + simpl. + destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. + right. + apply ZExtra.mod_0_bounds; try lia. + apply ZLib.Z_mod_mult'. + invert H20. + rewrite Z2Nat.id in H22; try lia. + apply Zmult_lt_compat_r with (p := 4) in H22; try lia. + rewrite ZLib.div_mul_undo in H22; try lia. + split; try lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + } + + rewrite <- EXPR_OK. + rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). + destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). + apply Z.mul_cancel_r with (p := 4) in e; try lia. + rewrite ZLib.div_mul_undo in e; try lia. + rewrite combine_lookup_first. + eapply H7; eauto. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. auto. + rewrite array_gso. + unfold array_get_error. + unfold arr_repeat. + simplify. + apply list_repeat_lookup. + lia. + unfold_constants. + intro. + apply Z2Nat.inj_iff in H21; try lia. + apply Z.div_pos; try lia. + apply Integers.Ptrofs.unsigned_range. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + unfold arr_stack_based_pointers. + intros. + destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). + + simplify. + erewrite Mem.load_store_same. + 2: { rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite e. + rewrite Integers.Ptrofs.unsigned_repr. + exact H1. + apply Integers.Ptrofs.unsigned_range_2. } + simplify. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. + destruct (Archi.ptr64); try discriminate. + pose proof (RSBP src). rewrite EQ_SRC in H0. + assumption. + + simpl. + erewrite Mem.load_store_other with (m1 := m). + 2: { exact H1. } + 2: { right. + rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite Integers.Ptrofs.unsigned_repr. + simpl. + destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. + right. + apply ZExtra.mod_0_bounds; try lia. + apply ZLib.Z_mod_mult'. + invert H0. + apply Zmult_lt_compat_r with (p := 4) in H21; try lia. + rewrite ZLib.div_mul_undo in H21; try lia. + split; try lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + } + apply ASBP; assumption. + + + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + rewrite ARCHI in H0. simplify. + + unfold check_address_parameter_unsigned in *; + unfold check_address_parameter_signed in *; simplify. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H1. clear ZERO. + rewrite Integers.Ptrofs.add_zero_l in H1. + + remember i0 as OFFSET. + + (** Read bounds assumption *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + (** Modular preservation proof *) + rename H0 into MOD_PRESERVE. + + (** Start of proof proper *) + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + apply assumption_32bit. + econstructor. econstructor. econstructor. + eapply Verilog.stmnt_runp_Vnonblock_arr. simplify. + econstructor. econstructor. econstructor. econstructor. + + all: simplify. + + (** State Lookup *) + unfold Verilog.merge_regs. + simplify. + unfold_merge. + apply AssocMap.gss. + + (** Match states *) + rewrite assumption_32bit. + econstructor; eauto. + + (** Match assocmaps *) + unfold Verilog.merge_regs. simplify. unfold_merge. + apply regs_lessdef_add_greater. apply greater_than_max_func. + assumption. + + (** States well formed *) + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. + apply AssocMap.gss. + + (** Match stacks *) + admit. + + (** Equality proof *) + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) + as EXPR_OK by admit. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. + + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + unfold Verilog.arr_assocmap_set. + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + rewrite AssocMap.gss. + setoid_rewrite H5. + reflexivity. + + rewrite combine_length. + rewrite <- array_set_len. + unfold arr_repeat. simplify. + apply list_repeat_len. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + rewrite H4. reflexivity. + + intros. + destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). + + erewrite Mem.load_store_same. + 2: { rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite e. + rewrite Integers.Ptrofs.unsigned_repr. + exact H1. + apply Integers.Ptrofs.unsigned_range_2. } + constructor. + erewrite combine_lookup_second. + simpl. + assert (Ple src (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H0 in H10. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H10; eauto. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. auto. + + assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). + rewrite Z.mul_comm in H10. + rewrite Z_div_mult in H10; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H10 by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in H10; unfold_constants; try lia. + rewrite H10. rewrite EXPR_OK. + rewrite array_get_error_set_bound. + reflexivity. + unfold arr_length, arr_repeat. simpl. + rewrite list_repeat_len. lia. + + erewrite Mem.load_store_other with (m1 := m). + 2: { exact H1. } + 2: { right. + rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite Integers.Ptrofs.unsigned_repr. + simpl. + destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. + right. + apply ZExtra.mod_0_bounds; try lia. + apply ZLib.Z_mod_mult'. + invert H8. + rewrite Z2Nat.id in H12; try lia. + apply Zmult_lt_compat_r with (p := 4) in H12; try lia. + rewrite ZLib.div_mul_undo in H12; try lia. + split; try lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + } + + rewrite <- EXPR_OK. + rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). + destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). + apply Z.mul_cancel_r with (p := 4) in e; try lia. + rewrite ZLib.div_mul_undo in e; try lia. + rewrite combine_lookup_first. + eapply H7; eauto. + + rewrite <- array_set_len. + unfold arr_repeat. simplify. + rewrite list_repeat_len. auto. + rewrite array_gso. + unfold array_get_error. + unfold arr_repeat. + simplify. + apply list_repeat_lookup. + lia. + unfold_constants. + intro. + apply Z2Nat.inj_iff in H10; try lia. + apply Z.div_pos; try lia. + apply Integers.Ptrofs.unsigned_range. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + unfold arr_stack_based_pointers. + intros. + destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). + + simplify. + erewrite Mem.load_store_same. + 2: { rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite e. + rewrite Integers.Ptrofs.unsigned_repr. + exact H1. + apply Integers.Ptrofs.unsigned_range_2. } + simplify. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. + destruct (Archi.ptr64); try discriminate. + pose proof (RSBP src). rewrite EQ_SRC in H0. + assumption. + + simpl. + erewrite Mem.load_store_other with (m1 := m). + 2: { exact H1. } + 2: { right. + rewrite ZERO. + rewrite Integers.Ptrofs.add_zero_l. + rewrite Integers.Ptrofs.unsigned_repr. + simpl. + destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. + right. + apply ZExtra.mod_0_bounds; try lia. + apply ZLib.Z_mod_mult'. + invert H0. + apply Zmult_lt_compat_r with (p := 4) in H10; try lia. + rewrite ZLib.div_mul_undo in H10; try lia. + split; try lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + } + apply ASBP; assumption. - eexists. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. + apply assumption_32bit. eapply Verilog.stmnt_runp_Vnonblock_reg with (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). @@ -411,41 +1880,101 @@ Section CORRECTNESS. constructor. apply boolToValue_ValueToBool. constructor. + unfold Verilog.merge_regs. unfold_merge. apply AssocMap.gss. destruct b. rewrite assumption_32bit. - apply match_state. + simplify. + apply match_state with (sp' := sp'); eauto. + unfold Verilog.merge_regs. unfold_merge. apply regs_lessdef_add_greater. apply greater_than_max_func. - assumption. assumption. + assumption. - unfold state_st_wf. intros. inversion H1. - subst. unfold_merge. + unfold state_st_wf. intros. + invert H3. + unfold Verilog.merge_regs. unfold_merge. apply AssocMap.gss. - assumption. + (** Match arrays *) + invert MARR. simplify. + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H4. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. assumption. rewrite assumption_32bit. - apply match_state. - unfold_merge. - apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. + apply match_state with (sp' := sp'); eauto. + unfold Verilog.merge_regs. unfold_merge. + apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. - unfold state_st_wf. intros. inversion H1. - subst. unfold_merge. + unfold state_st_wf. intros. + invert H1. + unfold Verilog.merge_regs. unfold_merge. apply AssocMap.gss. - assumption. + (** Match arrays *) + invert MARR. simplify. + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H2. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. assumption. + - admit. + - (* Return *) econstructor. split. eapply Smallstep.plus_two. eapply HTL.step_module; eauto. + apply assumption_32bit. constructor. econstructor; simpl; trivial. econstructor; simpl; trivial. @@ -453,9 +1982,9 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. - constructor. - constructor. + constructor. constructor. + unfold Verilog.merge_regs. unfold_merge. simpl. rewrite AssocMap.gso. rewrite AssocMap.gso. @@ -463,6 +1992,7 @@ Section CORRECTNESS. apply st_greater_than_res. apply st_greater_than_res. apply HTL.step_finish. + unfold Verilog.merge_regs. unfold_merge; simpl. rewrite AssocMap.gso. apply AssocMap.gss. @@ -470,12 +2000,14 @@ Section CORRECTNESS. apply AssocMap.gss. rewrite Events.E0_left. reflexivity. constructor. - assumption. + + admit. constructor. - econstructor. split. eapply Smallstep.plus_two. eapply HTL.step_module; eauto. + apply assumption_32bit. constructor. econstructor; simpl; trivial. econstructor; simpl; trivial. @@ -485,6 +2017,7 @@ Section CORRECTNESS. constructor. econstructor; simpl; trivial. apply Verilog.erun_Vvar. trivial. + unfold Verilog.merge_regs. unfold_merge. simpl. rewrite AssocMap.gso. rewrite AssocMap.gso. @@ -492,6 +2025,7 @@ Section CORRECTNESS. apply st_greater_than_res. apply st_greater_than_res. trivial. apply HTL.step_finish. + unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. @@ -499,27 +2033,71 @@ Section CORRECTNESS. apply AssocMap.gss. rewrite Events.E0_left. trivial. - constructor. assumption. simpl. inversion MASSOC. subst. + constructor. + admit. + + simpl. inversion MASSOC. subst. unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. apply st_greater_than_res. - inversion MSTATE; subst. inversion TF; subst. econstructor. split. apply Smallstep.plus_one. - eapply HTL.step_call. + eapply HTL.step_call. simplify. + + apply match_state with (sp' := stk); eauto. - constructor. apply regs_lessdef_add_greater. + apply regs_lessdef_add_greater. apply greater_than_max_func. - apply init_reg_assoc_empty. assumption. unfold state_st_wf. - intros. inv H1. apply AssocMap.gss. constructor. + apply init_reg_assoc_empty. + unfold state_st_wf. + intros. inv H3. apply AssocMap.gss. constructor. + + econstructor. simplify. + repeat split. unfold HTL.empty_stack. + simplify. apply AssocMap.gss. + unfold arr_repeat. simplify. + apply list_repeat_len. + intros. + destruct (Mem.load AST.Mint32 m' stk + (Integers.Ptrofs.unsigned (Integers.Ptrofs.add + Integers.Ptrofs.zero + (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. + pose proof Mem.load_alloc_same as LOAD_ALLOC. + pose proof H as ALLOC. + eapply LOAD_ALLOC in ALLOC. + 2: { exact LOAD. } + rewrite ALLOC. + repeat constructor. + constructor. - admit. + unfold reg_stack_based_pointers. intros. + unfold RTL.init_regs; simplify. + destruct (RTL.fn_params f); + rewrite Registers.Regmap.gi; constructor. + + unfold arr_stack_based_pointers. intros. + simplify. + destruct (Mem.load AST.Mint32 m' stk + (Integers.Ptrofs.unsigned (Integers.Ptrofs.add + Integers.Ptrofs.zero + (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. + pose proof Mem.load_alloc_same as LOAD_ALLOC. + pose proof H as ALLOC. + eapply LOAD_ALLOC in ALLOC. + 2: { exact LOAD. } + rewrite ALLOC. + repeat constructor. + constructor. - - inversion MSTATE; subst. inversion MS; subst. econstructor. + - invert MSTATE. invert MS. + econstructor. split. apply Smallstep.plus_one. constructor. - constructor; auto. constructor; auto. apply regs_lessdef_add_match; auto. + constructor; auto. + econstructor; auto. + apply regs_lessdef_add_match; auto. apply regs_lessdef_add_greater. apply greater_than_max_func. auto. unfold state_st_wf. intros. inv H. rewrite AssocMap.gso. @@ -530,8 +2108,6 @@ Section CORRECTNESS. Unshelve. exact (AssocMap.empty value). exact (AssocMap.empty value). - admit. - admit. (* exact (ZToValue 32 0). *) (* exact (AssocMap.empty value). *) (* exact (AssocMap.empty value). *) @@ -540,6 +2116,30 @@ Section CORRECTNESS. Admitted. Hint Resolve transl_step_correct : htlproof. + + Lemma option_inv : + forall A x y, + @Some A x = Some y -> x = y. + Proof. intros. inversion H. trivial. Qed. + + Lemma main_tprog_internal : + forall b, + Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> + exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f). + Proof. + intros. + destruct TRANSL. unfold main_is_internal in H1. + repeat (unfold_match H1). replace b with b0. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B. + unfold_match B. inv B. econstructor. apply A. + + apply option_inv. rewrite <- Heqo. rewrite <- H. + rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). + trivial. symmetry; eapply Linking.match_program_main; eauto. + Qed. + + (* Had to admit proof because currently there is no way to force main to be Internal. *) Lemma transl_initial_states : forall s1 : Smallstep.state (RTL.semantics prog), @@ -548,20 +2148,35 @@ Section CORRECTNESS. Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. Proof. induction 1. + destruct TRANSL. unfold main_is_internal in H4. + repeat (unfold_match H4). + assert (f = AST.Internal f1). apply option_inv. + rewrite <- Heqo0. rewrite <- H1. replace b with b0. + auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. + trivial. exploit function_ptr_translated; eauto. intros [tf [A B]]. unfold transl_fundef, Errors.bind in B. + unfold AST.transf_partial_fundef, Errors.bind in B. repeat (unfold_match B). inversion B. subst. + exploit main_tprog_internal; eauto; intros. + rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). + apply Heqo. symmetry; eapply Linking.match_program_main; eauto. + inversion H5. econstructor; split. econstructor. - apply (Genv.init_mem_transf_partial TRANSL); eauto. + apply (Genv.init_mem_transf_partial TRANSL'); eauto. replace (AST.prog_main tprog) with (AST.prog_main prog). rewrite symbols_preserved; eauto. symmetry; eapply Linking.match_program_main; eauto. - Admitted. - (*eexact A. trivial. + apply H6. + constructor. - apply transl_module_correct. auto. - Qed.*) + apply transl_module_correct. + assert (Some (AST.Internal x) = Some (AST.Internal m)). + replace (AST.fundef HTL.module) with (HTL.fundef). + rewrite <- H6. setoid_rewrite <- A. trivial. + trivial. inv H7. assumption. + Qed. Hint Resolve transl_initial_states : htlproof. Lemma transl_final_states : @@ -574,16 +2189,16 @@ Section CORRECTNESS. Proof. intros. inv H0. inv H. inv H4. inv MS. constructor. trivial. Qed. - Hint Resolve transl_final_states : htlproof.*) + Hint Resolve transl_final_states : htlproof. Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). Proof. -(* eapply Smallstep.forward_simulation_plus. + eapply Smallstep.forward_simulation_plus. apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. - exact transl_step_correct.*) -Admitted. + exact transl_step_correct. +Qed. End CORRECTNESS. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 887a696..a78256b 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -113,41 +113,13 @@ Ltac monadInv H := statemachine that is created by the translation contains the correct translations for each of the elements *) -Inductive tr_op : Op.operation -> list reg -> expr -> Prop := -| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r) -| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n)) -| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r)) -| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2) -| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2) -| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n) -| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2) -| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2) -| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2) -| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2) -| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2) -| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n) -| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2) -| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n) -| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2) -| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n) -| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r)) -| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2) -| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n) -| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2) -| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n) -| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e -| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e -| tr_op_Oleal : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Oleal a) l e -| tr_op_Ocast32signed : forall r, tr_op (Op.Ocast32signed) (r::nil) (Vvar r). -Hint Constructors tr_op : htlspec. - Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := | tr_instr_Inop : forall n, tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) | tr_instr_Iop : - forall n op args e dst, - tr_op op args e -> + forall n op args dst s s' e i, + translate_instr op args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) | tr_instr_Icond : forall n1 n2 cond args s s' i c, @@ -163,12 +135,16 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - | tr_instr_Iload : forall mem addr args s s' i c dst n, translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (block dst c) (state_goto st n) + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) | tr_instr_Istore : forall mem addr args s s' i c src n, translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vblock c (Vvar src)) - (state_goto st n). + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) + (state_goto st n) +| tr_instr_Ijumptable : + forall cexpr tbl r, + cexpr = tbl_to_case_expr st tbl -> + tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)). Hint Constructors tr_instr : htlspec. Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) @@ -184,14 +160,17 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk m start rst clk scldecls arrdecls, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls, (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> - tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> + tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> + stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> + Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk fin rtrn start rst clk scldecls arrdecls) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls) -> tr_module f m. Hint Constructors tr_module : htlspec. @@ -315,21 +294,6 @@ Ltac rewrite_states := remember (?x ?s) as c1; remember (?x ?s') as c2; try subst end. -Lemma translate_instr_tr_op : - forall op args s s' e i, - translate_instr op args s = OK e s' i -> - tr_op op args e. -Proof. -(* intros. - destruct op eqn:?; eauto with htlspec; try discriminate; simpl in *; - try (match goal with - [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] => - repeat (destruct args; try discriminate) - end); - monadInv H; constructor. -Qed.*) Admitted. (* FIXME: Currently admitted because added Osel *) -Hint Resolve translate_instr_tr_op : htlspec. - Ltac unfold_match H := match type of H with | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate @@ -343,7 +307,7 @@ Ltac inv_add_instr' H := end; repeat unfold_match H; inversion H. Ltac inv_add_instr := - match goal with + lazymatch goal with | H: context[add_instr_skip _ _ _] |- _ => inv_add_instr' H | H: context[add_instr_skip _ _] |- _ => @@ -356,6 +320,10 @@ Ltac inv_add_instr := inv_add_instr' H | H: context[add_branch_instr _ _ _ _] |- _ => monadInv H; inv_incr; inv_add_instr + | H: context[add_node_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_node_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr end. Ltac destruct_optional := @@ -370,7 +338,7 @@ Lemma iter_expand_instr_spec : c!pc = Some instr -> tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). Proof. -(* induction l; simpl; intros; try contradiction. + induction l; simpl; intros; try contradiction. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. destruct (peq pc pc1). - subst. @@ -383,15 +351,13 @@ Proof. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. unfold nonblock. assert (HST: st_st s4 = st_st s2) by congruence. rewrite HST. - constructor. eapply translate_instr_tr_op. apply EQ1. - eapply in_map with (f := fst) in H14. contradiction. + + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. + econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. rewrite <- e2. assert (HST: st_st s2 = st_st s0) by congruence. - rewrite HST. econstructor. apply EQ1. - eapply in_map with (f := fst) in H14. contradiction. + + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. + econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. @@ -409,6 +375,12 @@ Proof. eauto with htlspec. * apply in_map with (f := fst) in H2. contradiction. + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. + * inversion H14. constructor. congruence. + * apply in_map with (f := fst) in H14. contradiction. + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + inversion H2. @@ -428,10 +400,16 @@ Proof. - eapply IHl. apply EQ0. assumption. destruct H2. inversion H2. subst. contradiction. intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption.*) -Admitted. + destruct H2. inv H2. contradiction. assumption. assumption. +Qed. Hint Resolve iter_expand_instr_spec : htlspec. +Lemma create_arr_inv : forall w x y z a b c d, + create_arr w x y z = OK (a, b) c d -> y = b. +Proof. + inversion 1. reflexivity. +Qed. + Theorem transl_module_correct : forall f m, transl_module f = Errors.OK m -> tr_module f m. @@ -444,12 +422,22 @@ Proof. inversion s; subst. unfold transf_module in *. - monadInv Heqr. - econstructor; simpl; trivial. + unfold stack_correct in *. + destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; + destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; + destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; + simplify; + monadInv Heqr. + + (* TODO: We should be able to fold this into the automation. *) + pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. + rewrite <- STK_LEN. + + econstructor; simpl; auto. intros. inv_incr. assert (EQ3D := EQ3). - destruct x3. + destruct x4. apply collect_declare_datapath_trans in EQ3. apply collect_declare_controllogic_trans in EQ3D. assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index efe3565..b550ff9 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -29,13 +29,13 @@ Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item := match scldecl with - | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' + | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' | nil => nil end. Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item := match arrdecl with - | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' + | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' | nil => nil end. @@ -43,10 +43,10 @@ Definition transl_module (m : HTL.module) : Verilog.module := let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in let body := - Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) - :: Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1)) + Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1)) (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint))) (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in Verilog.mkmodule m.(mod_start) @@ -56,6 +56,7 @@ Definition transl_module (m : HTL.module) : Verilog.module := m.(mod_return) m.(mod_st) m.(mod_stk) + m.(mod_stk_len) m.(mod_params) body m.(mod_entrypoint). diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index 6c58c56..db96949 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -16,16 +16,66 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Import Smallstep. -From coqup Require HTL Verilog. +From compcert Require Import Smallstep Linking. +From coqup Require HTL. +From coqup Require Import Coquplib Veriloggen Verilog. + +Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := + match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. + +Lemma transf_program_match: + forall prog, match_prog prog (transl_program prog). +Proof. + intros. eapply match_transform_program_contextual. auto. +Qed. + +Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := +| match_stack : + forall res m pc reg_assoc arr_assoc hstk vstk, + match_stacks hstk vstk -> + match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) + (Stackframe res (transl_module m) pc + reg_assoc arr_assoc :: vstk) +| match_stack_nil : match_stacks nil nil. + +Inductive match_states : HTL.state -> state -> Prop := +| match_state : + forall m st reg_assoc arr_assoc hstk vstk, + match_stacks hstk vstk -> + match_states (HTL.State hstk m st reg_assoc arr_assoc) + (State vstk (transl_module m) st reg_assoc arr_assoc) +| match_returnstate : + forall v hstk vstk, + match_stacks hstk vstk -> + match_states (HTL.Returnstate hstk v) (Returnstate vstk v) +| match_initial_call : + forall m, + match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). Section CORRECTNESS. Variable prog: HTL.program. - Variable tprog: Verilog.program. + Variable tprog: program. + + Hypothesis TRANSL : match_prog prog tprog. + + Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. + + Theorem transl_step_correct : + forall (S1 : HTL.state) t S2, + HTL.step ge S1 t S2 -> + forall (R1 : state), + match_states S1 R1 -> + exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. + Proof. + induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split. + - apply Smallstep.plus_one. econstructor. eassumption. trivial. + * econstructor. econstructor. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). - Admitted. + End CORRECTNESS. + diff --git a/src/verilog/Array.v b/src/verilog/Array.v new file mode 100644 index 0000000..f3e1cd7 --- /dev/null +++ b/src/verilog/Array.v @@ -0,0 +1,324 @@ +Set Implicit Arguments. + +Require Import Lia. +Require Import Coquplib. +From Coq Require Import Lists.List Datatypes. + +Import ListNotations. + +Local Open Scope nat_scope. + +Record Array (A : Type) : Type := + mk_array + { arr_contents : list A + ; arr_length : nat + ; arr_wf : length arr_contents = arr_length + }. + +Definition make_array {A : Type} (l : list A) : Array A := + @mk_array A l (length l) eq_refl. + +Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A := + match i, l with + | _, nil => nil + | S n, h :: t => h :: list_set n x t + | O, h :: t => x :: t + end. + +Lemma list_set_spec1 {A : Type} : + forall l i (x : A), + i < length l -> nth_error (list_set i x l) i = Some x. +Proof. + induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder. +Qed. +Hint Resolve list_set_spec1 : array. + +Lemma list_set_spec2 {A : Type} : + forall l i (x : A) d, + i < length l -> nth i (list_set i x l) d = x. +Proof. + induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder. +Qed. +Hint Resolve list_set_spec2 : array. + +Lemma list_set_spec3 {A : Type} : + forall l i1 i2 (x : A), + i1 <> i2 -> + nth_error (list_set i1 x l) i2 = nth_error l i2. +Proof. + induction l; intros; destruct i1; destruct i2; simplify; try lia; try reflexivity; firstorder. +Qed. +Hint Resolve list_set_spec3 : array. + +Lemma array_set_wf {A : Type} : + forall l ln i (x : A), + length l = ln -> length (list_set i x l) = ln. +Proof. + induction l; intros; destruct i; auto. + + invert H; simplify; auto. +Qed. + +Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := + let l := a.(arr_contents) in + let ln := a.(arr_length) in + let WF := a.(arr_wf) in + @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF). + +Lemma array_set_spec1 {A : Type} : + forall a i (x : A), + i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x. +Proof. + intros. + + rewrite <- a.(arr_wf) in H. + unfold array_set. simplify. + eauto with array. +Qed. +Hint Resolve array_set_spec1 : array. + +Lemma array_set_spec2 {A : Type} : + forall a i (x : A) d, + i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x. +Proof. + intros. + + rewrite <- a.(arr_wf) in H. + unfold array_set. simplify. + eauto with array. +Qed. +Hint Resolve array_set_spec2 : array. + +Lemma array_set_len {A : Type} : + forall a i (x : A), + a.(arr_length) = (array_set i x a).(arr_length). +Proof. + unfold array_set. simplify. reflexivity. +Qed. + +Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A := + nth_error a.(arr_contents) i. + +Lemma array_get_error_equal {A : Type} : + forall (a b : Array A) i, + a.(arr_contents) = b.(arr_contents) -> + array_get_error i a = array_get_error i b. +Proof. + unfold array_get_error. congruence. +Qed. + +Lemma array_get_error_bound {A : Type} : + forall (a : Array A) i, + i < a.(arr_length) -> exists x, array_get_error i a = Some x. +Proof. + intros. + + rewrite <- a.(arr_wf) in H. + assert (~ length (arr_contents a) <= i) by lia. + + pose proof (nth_error_None a.(arr_contents) i). + apply not_iff_compat in H1. + apply <- H1 in H0. + + destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto. +Qed. + +Lemma array_get_error_set_bound {A : Type} : + forall (a : Array A) i x, + i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x. +Proof. + intros. + + unfold array_get_error. + eauto with array. +Qed. + +Lemma array_gso {A : Type} : + forall (a : Array A) i1 i2 x, + i1 <> i2 -> + array_get_error i2 (array_set i1 x a) = array_get_error i2 a. +Proof. + intros. + + unfold array_get_error. + unfold array_set. + simplify. + eauto with array. +Qed. + +Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A := + nth i a.(arr_contents) x. + +Lemma array_get_set_bound {A : Type} : + forall (a : Array A) i x d, + i < a.(arr_length) -> array_get i d (array_set i x a) = x. +Proof. + intros. + + unfold array_get. + info_eauto with array. +Qed. + +Lemma array_get_get_error {A : Type} : + forall (a : Array A) i x d, + array_get_error i a = Some x -> + array_get i d a = x. +Proof. + intros. + unfold array_get. + unfold array_get_error in H. + auto using nth_error_nth. +Qed. + +(** Tail recursive version of standard library function. *) +Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A := + match n with + | O => acc + | S n => list_repeat' (a::acc) a n + end. + +Lemma list_repeat'_len {A : Type} : forall (a : A) n l, + length (list_repeat' l a n) = (n + Datatypes.length l)%nat. +Proof. + induction n; intros; simplify; try reflexivity. + + specialize (IHn (a :: l)). + rewrite IHn. + simplify. + lia. +Qed. + +Lemma list_repeat'_app {A : Type} : forall (a : A) n l, + list_repeat' l a n = list_repeat' [] a n ++ l. +Proof. + induction n; intros; simplify; try reflexivity. + + pose proof IHn. + specialize (H (a :: l)). + rewrite H. clear H. + specialize (IHn (a :: nil)). + rewrite IHn. clear IHn. + remember (list_repeat' [] a n) as l0. + + rewrite <- app_assoc. + f_equal. +Qed. + +Lemma list_repeat'_head_tail {A : Type} : forall n (a : A), + a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]. +Proof. + induction n; intros; simplify; try reflexivity. + rewrite list_repeat'_app. + + replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]). + 2: { rewrite app_comm_cons. rewrite IHn; auto. + rewrite app_assoc. reflexivity. } + rewrite app_assoc. reflexivity. +Qed. + +Lemma list_repeat'_cons {A : Type} : forall (a : A) n, + list_repeat' [a] a n = a :: list_repeat' [] a n. +Proof. + intros. + + rewrite list_repeat'_head_tail; auto. + apply list_repeat'_app. +Qed. + +Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil. + +Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n. +Proof. + intros. + unfold list_repeat. + rewrite list_repeat'_len. + simplify. lia. +Qed. + +Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a', + (forall x x' : A, {x' = x} + {~ x' = x}) -> + In a' (list_repeat a n) -> a' = a. +Proof. + induction n; intros; simplify; try contradiction. + + unfold list_repeat in *. + simplify. + + rewrite list_repeat'_app in H. + pose proof (X a a'). + destruct H0; auto. + + (* This is actually a degenerate case, not an unprovable goal. *) + pose proof (in_app_or (list_repeat' [] a n) ([a])). + apply H0 in H. invert H. + + - eapply IHn in X; eassumption. + - invert H1; contradiction. +Qed. + +Lemma list_repeat_head_tail {A : Type} : forall n (a : A), + a :: list_repeat a n = list_repeat a n ++ [a]. +Proof. + unfold list_repeat. apply list_repeat'_head_tail. +Qed. + +Lemma list_repeat_cons {A : Type} : forall n (a : A), + list_repeat a (S n) = a :: list_repeat a n. +Proof. + intros. + + unfold list_repeat. + apply list_repeat'_cons. +Qed. + +Lemma list_repeat_lookup {A : Type} : + forall n i (a : A), + i < n -> + nth_error (list_repeat a n) i = Some a. +Proof. + induction n; intros. + + destruct i; simplify; lia. + + rewrite list_repeat_cons. + destruct i; simplify; firstorder. +Qed. + +Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n). + +Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C := + match x, y with + | a :: t, b :: t' => f a b :: list_combine f t t' + | _, _ => nil + end. + +Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B), + length (list_combine f x y) = min (length x) (length y). +Proof. + induction x; intros; simplify; try reflexivity. + + destruct y; simplify; auto. +Qed. + +Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C := + make_array (list_combine f x.(arr_contents) y.(arr_contents)). + +Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C), + x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length). +Proof. + intros. + + unfold combine. + unfold make_array. + simplify. + + rewrite <- (arr_wf x) in *. + rewrite <- (arr_wf y) in *. + + destruct (arr_contents x); simplify. + - reflexivity. + - destruct (arr_contents y); simplify. + f_equal. + rewrite list_combine_length. + destruct (Min.min_dec (length l) (length l0)); congruence. +Qed. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index c07d672..a3623f0 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -17,7 +17,7 @@ *) From Coq Require Import FSets.FMapPositive. -From coqup Require Import Coquplib Value AssocMap. +From coqup Require Import Coquplib Value AssocMap Array. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers Values. From compcert Require Import Maps. @@ -46,6 +46,7 @@ Record module: Type := mod_entrypoint : node; mod_st : reg; mod_stk : reg; + mod_stk_len : nat; mod_finish : reg; mod_return : reg; mod_start : reg; @@ -65,6 +66,9 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := | _, _ => empty_assocmap end. +Definition empty_stack (m : module) : Verilog.assocmap_arr := + (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. @@ -74,7 +78,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (assoc : assocmap), + (reg_assoc : Verilog.assocmap_reg) + (arr_assoc : Verilog.assocmap_arr), stackframe. Inductive state : Type := @@ -82,8 +87,8 @@ Inductive state : Type := forall (stack : list stackframe) (m : module) (st : node) - (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (list value)), state + (reg_assoc : Verilog.assocmap_reg) + (arr_assoc : Verilog.assocmap_arr), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -94,17 +99,19 @@ Inductive state : Type := Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g m st sf ctrl data + forall g m st sf ctrl data ist asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 asr' asa' f stval pstval, + asr!(m.(mod_st)) = Some ist -> + valueToPos ist = st -> m.(mod_controllogic)!st = Some ctrl -> m.(mod_datapath)!st = Some data -> Verilog.stmnt_runp f (Verilog.mkassociations asr empty_assocmap) - (Verilog.mkassociations asa (AssocMap.empty (list value))) + (Verilog.mkassociations asa (empty_stack m)) ctrl (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> @@ -114,8 +121,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := data (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> - asr' = merge_assocmap nasr2 basr2 -> - asa' = AssocMapExt.merge (list value) nasa2 basa2 -> + asr' = Verilog.merge_regs nasr2 basr2 -> + asa' = Verilog.merge_arrs nasa2 basa2 -> asr'!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') @@ -130,13 +137,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) (init_regs args m.(mod_params))) - (AssocMap.empty (list value))) + (empty_stack m)) | step_return : - forall g m asr i r sf pc mst, + forall g m asr asa i r sf pc mst, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) - (AssocMap.empty (list value))). + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := diff --git a/src/verilog/Value.v b/src/verilog/Value.v index d527b15..e7b2362 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -19,7 +19,7 @@ (* begin hide *) From bbv Require Import Word. From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith FSets.FMapPositive. +From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. (* end hide *) @@ -294,8 +294,18 @@ Inductive val_value_lessdef: val -> value -> Prop := forall i v', i = valueToInt v' -> val_value_lessdef (Vint i) v' +| val_value_lessdef_ptr: + forall b off v', + off = Ptrofs.repr (valueToZ v') -> + (Z.modulo (valueToZ v') 4) = 0%Z -> + val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. +Inductive opt_val_value_lessdef: option val -> value -> Prop := +| opt_lessdef_some: + forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' +| opt_lessdef_none: forall v, opt_val_value_lessdef None v. + Lemma valueToZ_ZToValue : forall n z, (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> @@ -330,7 +340,19 @@ Proof. rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. split. apply Zle_0_pos. - assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt. + assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. + inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. + simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. +Qed. + +Lemma valueToPos_posToValue : + forall p, valueToPos (posToValueAuto p) = p. +Proof. + intros. unfold valueToPos, posToValueAuto. + rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. + split. apply Zle_0_pos. + + assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. Qed. @@ -361,3 +383,18 @@ Lemma boolToValue_ValueToBool : forall b, valueToBool (boolToValue 32 b) = b. Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. + +(*Lemma ZToValue_valueToNat : + forall x sz, + sz > 0 -> + (x < 2^(Z.of_nat sz))%Z -> + valueToNat (ZToValue sz x) = Z.to_nat x. +Proof. + destruct x; intros; unfold ZToValue, valueToNat; simpl. + - rewrite wzero'_def. apply wordToNat_wzero. + - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. + unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0. + rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z. + Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *) + Search "inj" positive nat. +*) diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index b80678e..555ddbd 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -25,9 +25,11 @@ From Coq Require Import Lists.List Program. +Require Import Lia. + Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap. +From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array. From compcert Require Integers Events. From compcert Require Import Errors Smallstep Globalenvs. @@ -47,39 +49,51 @@ Record associations (A : Type) : Type := assoc_nonblocking : AssocMap.t A }. +Definition arr := (Array (option value)). + Definition reg_associations := associations value. -Definition arr_associations := associations (list value). +Definition arr_associations := associations arr. -Definition assocmap_arr := AssocMap.t (list value). +Definition assocmap_reg := AssocMap.t value. +Definition assocmap_arr := AssocMap.t arr. -Definition merge_associations {A : Type} (assoc : associations A) := - mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking)) - (AssocMap.empty A). +Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg := + AssocMapExt.merge value new old. + +Definition merge_cell (new : option value) (old : option value) : option value := + match new, old with + | Some _, _ => new + | _, _ => old + end. + +Definition merge_arr (new : option arr) (old : option arr) : option arr := + match new, old with + | Some new', Some old' => Some (combine merge_cell new' old') + | Some new', None => Some new' + | None, Some old' => Some old' + | None, None => None + end. + +Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr := + AssocMap.combine merge_arr new old. Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := match a ! r with | None => None - | Some arr => nth_error arr i - end. - -Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A := - match i, l with - | _, nil => nil - | S n, h :: t => h :: list_set n x t - | O, h :: t => x :: t + | Some arr => Some (Option.default (NToValue 32 0) (Option.join (array_get_error i arr))) end. -Definition assocmap_l_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := +Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := match a ! r with | None => a - | Some arr => AssocMap.set r (list_set i v arr) a + | Some arr => a # r <- (array_set i (Some v) arr) end. Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := - mkassociations (assocmap_l_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). + mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := - mkassociations asa.(assoc_blocking) (assocmap_l_set r i v asa.(assoc_nonblocking)). + mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)). Definition block_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking). @@ -87,8 +101,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) := Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). -Inductive scl_decl : Type := Scalar (sz : nat). -Inductive arr_decl : Type := Array (sz : nat) (ln : nat). +Inductive scl_decl : Type := VScalar (sz : nat). +Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). (** * Verilog AST @@ -218,6 +232,7 @@ Record module : Type := mkmodule { mod_return : reg; mod_st : reg; (**r Variable that defines the current state, it should be internal. *) mod_stk : reg; + mod_stk_len : nat; mod_args : list reg; mod_body : list module_item; mod_entrypoint : node; @@ -235,7 +250,7 @@ Definition posToLit (p : positive) : expr := Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. -Definition fext := AssocMap.t value. +Definition fext := assocmap. Definition fextclk := nat -> fext. (** ** State @@ -264,7 +279,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (assoc : assocmap), + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), stackframe. Inductive state : Type := @@ -272,8 +288,8 @@ Inductive state : Type := forall (stack : list stackframe) (m : module) (st : node) - (reg_assoc : assocmap) - (arr_assoc : AssocMap.t (list value)), state + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), state | Returnstate : forall (res : list stackframe) (v : value), state @@ -691,17 +707,21 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := end. Definition genv := Globalenvs.Genv.t fundef unit. +Definition empty_stack (m : module) : assocmap_arr := + (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)). Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g, + forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, + asr!(m.(mod_st)) = Some ist -> + valueToPos ist = st -> mis_stepp f (mkassociations asr empty_assocmap) - (mkassociations asa (AssocMap.empty (list value))) + (mkassociations asa (empty_stack m)) m.(mod_body) (mkassociations basr1 nasr1) (mkassociations basa1 nasa1)-> - asr' = merge_assocmap nasr1 basr1 -> - asa' = AssocMapExt.merge (list value) nasa1 basa1 -> + asr' = merge_regs nasr1 basr1 -> + asa' = merge_arrs nasa1 basa1 -> asr'!(m.(mod_st)) = Some stval -> valueToPos stval = pstval -> step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') @@ -716,13 +736,13 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint)) (init_params args m.(mod_args))) - (AssocMap.empty (list value))) + (empty_stack m)) | step_return : - forall g m asr i r sf pc mst, + forall g m asr i r sf pc mst asa, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) - (AssocMap.empty (list value))). + (empty_stack m)). Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := |