Add support for more assembly

I want to be able to handle the output of gcc/clang on our C code.

Right now, I have added support for parsing the assembly output.
Equivalence checking is still to come.

src/Assembly/Equality.v

@@ -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.
@@ -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.
@@ -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.
@@ -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.
@@ -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.

src/Assembly/Equivalence.v

@@ -4,6 +4,7 @@ From Coq Require Import ZArith.
 From Coq Require Import NArith.
 Require Import Crypto.Assembly.Syntax.
 Require Import Crypto.Assembly.Parse.
+Require Import Crypto.Assembly.Equality.
 Require Import Crypto.Assembly.Symbolic.
 Require Import Crypto.Util.Strings.Parse.Common.
 Require Import Crypto.Util.ErrorT.
@@ -277,8 +278,8 @@ Definition show_annotated_Line : Show AnnotatedLine
               end)%string.
 
 Global Instance show_lines_AnnotatedLines : ShowLines AnnotatedLines
-  := fun '(ls, ss)
-     => let d := dag.eager.force ss.(dag_state) in
+  := fun '(ls, sst)
+     => let d := dag.eager.force sst.(dag_state) in
         List.map (fun l => show_annotated_Line (l, d)) ls.
 
 Fixpoint remove_common_indices {T} (eqb : T -> T -> bool) (xs ys : list T) (start_idx : nat) : list (nat * T) * list T
@@ -731,11 +732,11 @@ Global Instance show_lines_EquivalenceCheckingError : ShowLines EquivalenceCheck
 Global Instance show_EquivalenceCheckingError : Show EquivalenceCheckingError
   := fun err => String.concat String.NewLine (show_lines err).
 
-Definition merge_fresh_symbol {descr:description} : dag.M idx := fun d => merge_node (dag.gensym 64%N d) d.
+Definition merge_fresh_symbol {descr:description} (sz : OperationSize) : dag.M idx := fun d => merge_node (dag.gensym sz d) d.
 Definition merge_literal {descr:description} (l:Z) : dag.M idx := merge_node ((const l, nil)).
 
 Definition SetRegFresh {opts : symbolic_options_computed_opt} {descr:description} (r : REG) : M idx :=
-  (idx <- lift_dag merge_fresh_symbol;
+  (idx <- lift_dag (merge_fresh_symbol (widest_reg_size_of r));
   _ <- SetReg r idx;
   Symbolic.ret idx).
 
@@ -812,13 +813,13 @@ Fixpoint simplify_input_type
      end%error.
 
 Definition build_inputarray {descr:description} (len : nat) : dag.M (list idx) :=
-  List.foldmap (fun _ => merge_fresh_symbol) (List.seq 0 len).
+  List.foldmap (fun _ => merge_fresh_symbol 64%N) (List.seq 0 len).
 
 Fixpoint build_inputs {descr:description} (types : type_spec) : dag.M (list (idx + list idx))
   := match types with
      | [] => dag.ret []
      | None :: tys
-       => (idx <- merge_fresh_symbol;
+       => (idx <- merge_fresh_symbol 64%N;
            rest <- build_inputs tys;
            dag.ret (inl idx :: rest))
      | Some len :: tys
@@ -858,12 +859,12 @@ Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {desc
            Symbolic.ret (inl addr :: rest))
      end%N%x86symex.
 
-Fixpoint dag_gensym_n {descr:description} (n : nat) : dag.M (list symbol) :=
-  match n with
-  | O => dag.ret nil
-  | S n =>
-      (i <- merge_fresh_symbol;
-       rest <- dag_gensym_n n;
+Fixpoint dag_gensym_ls {descr:description} (ls : list OperationSize) : dag.M (list symbol) :=
+  match ls with
+  | nil => dag.ret nil
+  | sz :: ls =>
+      (i <- merge_fresh_symbol sz;
+       rest <- dag_gensym_ls ls;
        dag.ret (cons i rest))
   end%dagM.
 
@@ -1275,10 +1276,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_ls (List.map reg_size 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;
      |}.