Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Use Listable to prove equality of registers and opcodes #2020

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
+365 −266
Draft

Use Listable to prove equality of registers and opcodes #2020

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 10 additions & 10 deletions src/Assembly/Equality.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ Bind Scope REG_scope with REG.
Infix "=?" := REG_beq : REG_scope.

Global Instance REG_beq_spec : reflect_rel (@eq REG) REG_beq | 10
:= reflect_of_beq internal_REG_dec_bl internal_REG_dec_lb.
Definition REG_beq_eq x y : (x =? y)%REG = true <-> x = y := conj (@internal_REG_dec_bl _ _) (@internal_REG_dec_lb _ _).
:= reflect_of_beq REG_dec_bl REG_dec_lb.
Definition REG_beq_eq x y : (x =? y)%REG = true <-> x = y := conj (@REG_dec_bl _ _) (@REG_dec_lb _ _).
Lemma REG_beq_neq x y : (x =? y)%REG = false <-> x <> y.
Proof. rewrite <- REG_beq_eq; destruct (x =? y)%REG; intuition congruence. Qed.
Global Instance REG_beq_compat : Proper (eq ==> eq ==> eq) REG_beq | 10.
Expand Down Expand Up @@ -95,8 +95,8 @@ Bind Scope AccessSize_scope with AccessSize.
Infix "=?" := AccessSize_beq : AccessSize_scope.

Global Instance AccessSize_beq_spec : reflect_rel (@eq AccessSize) AccessSize_beq | 10
:= reflect_of_beq internal_AccessSize_dec_bl internal_AccessSize_dec_lb.
Definition AccessSize_beq_eq x y : (x =? y)%AccessSize = true <-> x = y := conj (@internal_AccessSize_dec_bl _ _) (@internal_AccessSize_dec_lb _ _).
:= reflect_of_beq AccessSize_dec_bl AccessSize_dec_lb.
Definition AccessSize_beq_eq x y : (x =? y)%AccessSize = true <-> x = y := conj (@AccessSize_dec_bl _ _) (@AccessSize_dec_lb _ _).
Lemma AccessSize_beq_neq x y : (x =? y)%AccessSize = false <-> x <> y.
Proof. rewrite <- AccessSize_beq_eq; destruct (x =? y)%AccessSize; intuition congruence. Qed.
Global Instance AccessSize_beq_compat : Proper (eq ==> eq ==> eq) AccessSize_beq | 10.
Expand Down Expand Up @@ -141,8 +141,8 @@ Bind Scope FLAG_scope with FLAG.
Infix "=?" := FLAG_beq : FLAG_scope.

Global Instance FLAG_beq_spec : reflect_rel (@eq FLAG) FLAG_beq | 10
:= reflect_of_beq internal_FLAG_dec_bl internal_FLAG_dec_lb.
Definition FLAG_beq_eq x y : (x =? y)%FLAG = true <-> x = y := conj (@internal_FLAG_dec_bl _ _) (@internal_FLAG_dec_lb _ _).
:= reflect_of_beq FLAG_dec_bl FLAG_dec_lb.
Definition FLAG_beq_eq x y : (x =? y)%FLAG = true <-> x = y := conj (@FLAG_dec_bl _ _) (@FLAG_dec_lb _ _).
Lemma FLAG_beq_neq x y : (x =? y)%FLAG = false <-> x <> y.
Proof. rewrite <- FLAG_beq_eq; destruct (x =? y)%FLAG; intuition congruence. Qed.
Global Instance FLAG_beq_compat : Proper (eq ==> eq ==> eq) FLAG_beq | 10.
Expand All @@ -155,8 +155,8 @@ Bind Scope OpCode_scope with OpCode.
Infix "=?" := OpCode_beq : OpCode_scope.

Global Instance OpCode_beq_spec : reflect_rel (@eq OpCode) OpCode_beq | 10
:= reflect_of_beq internal_OpCode_dec_bl internal_OpCode_dec_lb.
Definition OpCode_beq_eq x y : (x =? y)%OpCode = true <-> x = y := conj (@internal_OpCode_dec_bl _ _) (@internal_OpCode_dec_lb _ _).
:= reflect_of_beq OpCode_dec_bl OpCode_dec_lb.
Definition OpCode_beq_eq x y : (x =? y)%OpCode = true <-> x = y := conj (@OpCode_dec_bl _ _) (@OpCode_dec_lb _ _).
Lemma OpCode_beq_neq x y : (x =? y)%OpCode = false <-> x <> y.
Proof. rewrite <- OpCode_beq_eq; destruct (x =? y)%OpCode; intuition congruence. Qed.
Global Instance OpCode_beq_compat : Proper (eq ==> eq ==> eq) OpCode_beq | 10.
Expand All @@ -169,8 +169,8 @@ Bind Scope OpPrefix_scope with OpPrefix.
Infix "=?" := OpPrefix_beq : OpPrefix_scope.

Global Instance OpPrefix_beq_spec : reflect_rel (@eq OpPrefix) OpPrefix_beq | 10
:= reflect_of_beq internal_OpPrefix_dec_bl internal_OpPrefix_dec_lb.
Definition OpPrefix_beq_eq x y : (x =? y)%OpPrefix = true <-> x = y := conj (@internal_OpPrefix_dec_bl _ _) (@internal_OpPrefix_dec_lb _ _).
:= reflect_of_beq OpPrefix_dec_bl OpPrefix_dec_lb.
Definition OpPrefix_beq_eq x y : (x =? y)%OpPrefix = true <-> x = y := conj (@OpPrefix_dec_bl _ _) (@OpPrefix_dec_lb _ _).
Lemma OpPrefix_beq_neq x y : (x =? y)%OpPrefix = false <-> x <> y.
Proof. rewrite <- OpPrefix_beq_eq; destruct (x =? y)%OpPrefix; intuition congruence. Qed.
Global Instance OpPrefix_beq_compat : Proper (eq ==> eq ==> eq) OpPrefix_beq | 10.
Expand Down
4 changes: 2 additions & 2 deletions src/Assembly/Equivalence.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1275,10 +1275,10 @@ Definition init_symbolic_state_descr : description := Build_description "init_sy

Definition init_symbolic_state (d : dag) : symbolic_state
:= let _ := init_symbolic_state_descr in
let '(initial_reg_idxs, d) := dag_gensym_n 16 d in
let '(initial_reg_idxs, d) := dag_gensym_n (List.length widest_registers) d in
{|
dag_state := d;
symbolic_reg_state := Tuple.from_list_default None 16 (List.map Some initial_reg_idxs);
symbolic_reg_state := Tuple.from_list_default None _ (List.map Some initial_reg_idxs);
symbolic_mem_state := [];
symbolic_flag_state := Tuple.repeat None 6;
|}.
Expand Down
4 changes: 2 additions & 2 deletions src/Assembly/EquivalenceProofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1847,7 +1847,7 @@ Qed.
(* TODO: this is Symbolic.get_reg; move to SymbolicProofs? *)
Lemma get_reg_set_reg_full s rn rn' v
: get_reg (set_reg s rn v) rn'
= if ((rn <? ((fun n (_ : Tuple.tuple _ n) => n) _ s)) && (rn =? rn'))%nat%bool
= if ((rn <? ((fun n (_ : Tuple.tuple _ n) => N.of_nat n) _ s)) && (rn =? rn'))%N%bool
then Some v
else get_reg s rn'.
Proof.
Expand All @@ -1863,7 +1863,7 @@ Qed.

(* TODO: this is Symbolic.get_reg; move to SymbolicProofs? *)
Local Lemma get_reg_set_reg_same s rn v
(H : (rn < (fun n (_ : Tuple.tuple _ n) => n) _ s)%nat)
(H : (rn < (fun n (_ : Tuple.tuple _ n) => N.of_nat n) _ s)%N)
: get_reg (set_reg s rn v) rn = Some v.
Proof.
rewrite get_reg_set_reg_full; break_innermost_match; reflect_hyps; cbv beta in *; try reflexivity; lia.
Expand Down
20 changes: 0 additions & 20 deletions src/Assembly/Parse.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,34 +22,18 @@ Local Open Scope list_scope.
Local Open Scope string_scope.
Local Open Scope parse_scope.

Derive REG_Listable SuchThat (@FinitelyListable REG REG_Listable) As REG_FinitelyListable.
Proof. prove_ListableDerive. Qed.
Global Existing Instances REG_Listable REG_FinitelyListable.

Global Instance show_REG : Show REG.
Proof. prove_Show_enum (). Defined.
Global Instance show_lvl_REG : ShowLevel REG := show_REG.

Derive FLAG_Listable SuchThat (@FinitelyListable FLAG FLAG_Listable) As FLAG_FinitelyListable.
Proof. prove_ListableDerive. Qed.
Global Existing Instances FLAG_Listable FLAG_FinitelyListable.

Global Instance show_FLAG : Show FLAG.
Proof. prove_Show_enum (). Defined.
Global Instance show_lvl_FLAG : ShowLevel FLAG := show_FLAG.

Derive OpCode_Listable SuchThat (@FinitelyListable OpCode OpCode_Listable) As OpCode_FinitelyListable.
Proof. prove_ListableDerive. Qed.
Global Existing Instances OpCode_Listable OpCode_FinitelyListable.

Global Instance show_OpCode : Show OpCode.
Proof. prove_Show_enum (). Defined.
Global Instance show_lvl_OpCode : ShowLevel OpCode := show_OpCode.

Derive OpPrefix_Listable SuchThat (@FinitelyListable OpPrefix OpPrefix_Listable) As OpPrefix_FinitelyListable.
Proof. prove_ListableDerive. Qed.
Global Existing Instances OpPrefix_Listable OpPrefix_FinitelyListable.

Global Instance show_OpPrefix : Show OpPrefix.
Proof. prove_Show_enum (). Defined.
Global Instance show_lvl_OpPrefix : ShowLevel OpPrefix := show_OpPrefix.
Expand All @@ -72,10 +56,6 @@ Definition parse_FLAG_list : list (string * FLAG)
Definition parse_FLAG : ParserAction FLAG
:= parse_strs parse_FLAG_list.

Derive AccessSize_Listable SuchThat (@FinitelyListable AccessSize AccessSize_Listable) As AccessSize_FinitelyListable.
Proof. prove_ListableDerive. Qed.
Global Existing Instances AccessSize_Listable AccessSize_FinitelyListable.

Global Instance show_AccessSize : Show AccessSize.
Proof. prove_Show_enum (). Defined.
Global Instance show_lvl_AccessSize : ShowLevel AccessSize := show_AccessSize.
Expand Down
20 changes: 10 additions & 10 deletions src/Assembly/Symbolic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3829,7 +3829,7 @@ Definition simplify {opts : symbolic_options_computed_opt} (dag : dag) (e : node
Lemma eval_simplify {opts : symbolic_options_computed_opt} G d n v : gensym_dag_ok G d -> eval_node G d n v -> eval G d (simplify d n) v.
Proof using Type. eauto using Rewrite.eval_expr, eval_node_reveal_node_at_least. Qed.

Definition reg_state := Tuple.tuple (option idx) 16.
Definition reg_state := Tuple.tuple (option idx) (compute! (List.length widest_registers)).
Definition flag_state := Tuple.tuple (option idx) 6.
Definition mem_state := list (idx * idx).

Expand Down Expand Up @@ -3863,16 +3863,16 @@ Definition reverse_lookup_flag (st : flag_state) (i : idx) : option FLAG
(List.find (fun v => option_beq N.eqb (Some i) (fst v))
(Tuple.to_list _ (Tuple.map2 (@pair _ _) st (CF, PF, AF, ZF, SF, OF)))).

Definition get_reg (st : reg_state) (ri : nat) : option idx
:= Tuple.nth_default None ri st.
Definition set_reg (st : reg_state) ri (i : idx) : reg_state
Definition get_reg (st : reg_state) (ri : N) : option idx
:= Tuple.nth_default None (N.to_nat ri) st.
Definition set_reg (st : reg_state) (ri : N) (i : idx) : reg_state
:= Tuple.from_list_default None _ (ListUtil.set_nth
ri
(N.to_nat ri)
(Some i)
(Tuple.to_list _ st)).
Definition reverse_lookup_widest_reg (st : reg_state) (i : idx) : option REG
:= option_map
(fun v => widest_register_of_index (fst v))
(fun v => widest_register_of_index (N.of_nat (fst v)))
(List.find (fun v => option_beq N.eqb (Some i) (snd v))
(List.enumerate (Tuple.to_list _ st))).

Expand Down Expand Up @@ -3906,7 +3906,7 @@ Definition update_mem_with (st : symbolic_state) (f : mem_state -> mem_state) :
:= {| dag_state := st.(dag_state); symbolic_reg_state := st.(symbolic_reg_state) ; symbolic_flag_state := st.(symbolic_flag_state) ; symbolic_mem_state := f st.(symbolic_mem_state) |}.

Global Instance show_reg_state : Show reg_state := fun st =>
show (List.map (fun '(n, v) => (widest_register_of_index n, v)) (ListUtil.List.enumerate (Option.List.map id (Tuple.to_list _ st)))).
show (List.combine widest_registers (Option.List.map id (Tuple.to_list _ st))).

Global Instance show_flag_state : Show flag_state :=
fun '(cfv, pfv, afv, zfv, sfv, ofv) => (
Expand Down Expand Up @@ -3953,7 +3953,7 @@ Module error.
Local Unset Decidable Equality Schemes.
Variant error :=
| get_flag (f : FLAG) (s : flag_state)
| get_reg (r : nat + REG) (s : reg_state)
| get_reg (r : N + REG) (s : reg_state)
| load (a : idx) (s : symbolic_state)
| remove (a : idx) (s : symbolic_state)
| remove_has_duplicates (a : idx) (vs : list idx) (s : symbolic_state)
Expand All @@ -3977,7 +3977,7 @@ Module error.
=> ["In flag state " ++ show_flag_state s;
"Flag " ++ show f ++ " was read without being set."]
| get_reg (inl i) s
=> ["Invalid reg index " ++ show_nat i]
=> ["Invalid reg index " ++ show i]
| get_reg (inr r) s
=> ["In reg state " ++ show_reg_state s;
"Register " ++ show (r : REG) ++ " read without being set."]
Expand Down Expand Up @@ -4042,7 +4042,7 @@ Definition mapM_ {A B} (f: A -> M B) l : M unit := _ <- mapM f l; ret tt.

Definition error_get_reg_of_reg_index ri : symbolic_state -> error
:= error.get_reg (let r := widest_register_of_index ri in
if (reg_index r =? ri)%nat
if (reg_index r =? ri)%N
then inr r
else inl ri).

Expand Down
Loading