Avoid decidable equality for type indices in binary op case of symbolic term equality function

[skeuchel]

In our function for testing for equality of two symbolic terms of the same type,

katamaran/theories/Syntax/Terms.v

Lines 296 to 322 in 26a30b5

	Equations(noeqns) Term_eqb {Σ} [σ : Ty] (t1 t2 : Term Σ σ) : bool :=
	Term_eqb (@term_var _ _ ς1inΣ) (@term_var _ _ ς2inΣ) :=
	ctx.In_eqb ς1inΣ ς2inΣ;
	Term_eqb (term_val _ v1) (term_val _ v2) :=
	if eq_dec v1 v2 then true else false;
	Term_eqb (term_binop op1 x1 y1) (term_binop op2 x2 y2)
	with bop.eqdep_dec op1 op2 => {
	Term_eqb (term_binop op1 x1 y1) (term_binop ?(op1) x2 y2) (left bop.opeq_refl) :=
	Term_eqb x1 x2 &&& Term_eqb y1 y2;
	Term_eqb (term_binop op1 x1 y1) (term_binop op2 x2 y2) (right _) := false
	};
	Term_eqb (term_unop op1 t1) (term_unop op2 t2) with uop.tel_eq_dec op1 op2 => {
	Term_eqb (term_unop op1 t1) (term_unop ?(op1) t2) (left eq_refl) :=
	Term_eqb t1 t2;
	Term_eqb (term_unop op1 t1) (term_unop op2 t2) (right _) := false;
	};
	Term_eqb (@term_tuple ?(σs) xs) (@term_tuple σs ys) :=
	@env.eqb_hom _ (Term Σ) (@Term_eqb _) _ xs ys;
	Term_eqb (@term_union ?(u) _ k1 e1) (@term_union u _ k2 e2)
	with eq_dec k1 k2 => {
	Term_eqb (term_union k1 e1) (term_union ?(k1) e2) (left eq_refl) :=
	Term_eqb e1 e2;
	Term_eqb _ _ (right _) := false
	};
	Term_eqb (@term_record ?(r) xs) (@term_record r ys) :=
	@env.eqb_hom _ (fun b => Term Σ (type b)) (fun b => @Term_eqb _ (type b)) _ xs ys;
	Term_eqb _ _ := false.

we throw exactly that information away in the binary op case and rather implement fully heterogenous decidable equality for binops

katamaran/theories/Syntax/BinOps.v

Lines 145 to 147 in 26a30b5

	Definition binoptel_eq_dec {σ1 σ2 σ3 τ1 τ2 τ3 : Ty}
	(op1 : BinOp σ1 σ2 σ3) (op2 : BinOp τ1 τ2 τ3) :
	dec_eq (A := BinOpTel) ((σ1,σ2,σ3),op1) ((τ1,τ2,τ3),op2) :=

which for instance tests equality of the components of a product type, even if we already knew that the results, i.e. the product types, were equal!

katamaran/theories/Syntax/BinOps.v

Lines 156 to 157 in 26a30b5

	| @pair _ σ1 σ2 , @pair _ τ1 τ2 =>
	f_equal2_dec binoptel_pair (ninv _ _) (eq_dec σ1 τ1) (eq_dec σ2 τ2)

These additional equality checks of types, or more generally part of the type index of symbolic terms like for instance natural numbers for the bitvector length, can block metalevel computation when running the symbolic executor on polymorphic functions, i.e. functions with some form of quantification at the metalevel. For instance, the verification of the to_bits function from the RISC-V case study, critically relies on the fact that the term equality in the unary op case does not use decidable equality on the metalevel bitvector length

katamaran/case_study/RiscvPmp/Machine.v

Lines 536 to 537 in 26a30b5

	Definition fun_to_bits (l : nat) : Stm [value :: ty.int] (ty.bvec l) :=
	exp_get_slice_int value.

The decidable equality check is correctly implemented for unary ops, i.e. we propagate the information that the result type of the two unary ops being compared is the same

katamaran/theories/Syntax/UnOps.v

Lines 86 to 88 in 26a30b5

	#[derive(equations=no)] Equations tel_eq_dec {σ1 σ2 τ : Ty}
	(op1 : UnOp σ1 τ) (op2 : UnOp σ2 τ) :
	dec_eq (A := Tel τ) (σ1,op1) (σ2,op2) :=

I propose to implement the same for binary ops.

However, this is more difficult for binary ops because of the green slime in the indices

katamaran/theories/Syntax/BinOps.v

Lines 81 to 82 in 26a30b5

	| bvapp {m n} : BinOp (bvec m) (bvec n) (bvec (m + n))
	| bvcons {m} : BinOp (bool) (bvec m) (bvec (S m))

Trying to implement it in the same way as for unary ops using the equations package fails with an error message that a covering cannot be found.