Get Coq extraction working with the latest Coq version

[eddywestbrook]

Right now, the saw-core-coq Coq extraction does not work with the latest version of Coq. Instead, the README in that directory suggests using Coq version 8.12. I don't remember exactly whether the issue is that generated Coq files do not work with the newer version of Coq or that the existing handwritten Coq library files do not work, but either way this should be fixed.

[robdockins]

What version of Coq are you having problems with? It works for me with Coq 8.13.2.

[eddywestbrook]

Yeah, actually, it seems to be working for me with Coq 8.13.1 now too. I think maybe the problem was originally that the coq-bits library didn't yet support Coq versions past 8.12, but they put out a new version that supports through 8.14. So... maybe we should close this?

[RyanGlScott]

I finally had a chance to try building saw-core-coq's Coq library with Coq 8.14.1, and there is a legitimate issue that prevents it from building:

$ make
COQC generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v

<snip>

File "./generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v", line 624, characters 0-1536:
Error:
The following term contains unresolved implicit arguments:
  (finNumRec
     (fun n : Num =>
      forall ix : Type, PIntegral ix -> seq n Bool -> ix -> seq n Bool)
     (fun (n : Nat) (ix : Type)
        (pix : RecordTypeCons "div" (ix -> ix -> ix)
                 (RecordTypeCons "integralRing"
                    (RecordTypeCons "add" (ix -> ix -> ix)
                       (RecordTypeCons "int" (Integer -> ix)
                          (RecordTypeCons "mul" (ix -> ix -> ix)
                             (RecordTypeCons "neg" 
                                (ix -> ix)
                                (RecordTypeCons "ringZero" ix
                                   (RecordTypeCons "sub" 
                                      (ix -> ix -> ix) RecordTypeNil))))))
                    (RecordTypeCons "mod" (ix -> ix -> ix)
                       (RecordTypeCons "posNegCases"
                          (forall r : Type,
                           (Nat -> r) -> (Nat -> r) -> ix -> r)
                          (RecordTypeCons "toInt" 
                             (ix -> Integer) RecordTypeNil))))) =>
      natCase (fun w : Nat => bitvector w -> ix -> bitvector w)
        (fun (xs : bitvector 0) (_ : ix) => xs)
        (fun (w : Nat) (xs : bitvector (Succ w)) =>
         let var__0 := Succ w in
         RecordProj pix "posNegCases" (bitvector var__0) 
           (bvSShr w xs) (bvShl var__0 xs)) n))
More precisely: 
- ?Inh_p: Cannot infer the implicit parameter Inh_p of finNumRec whose type
  is
  "forall _1 : Num,
   Inhabited
     ((fun n : Num =>
       forall ix : Type, PIntegral ix -> seq n Bool -> ix -> seq n Bool) _1)"
  (no type class instance found).

make[1]: *** [Makefile.coq:763: generated/CryptolToCoq/CryptolPrimitivesForSAWCore.vo] Error 1
make: *** [Makefile.coq:386: all] Error 2

[eddywestbrook]

They must have changed something about how typeclass resolution is performed. It seems like that beta-redex in the argument to Inhabited should reduce, but somehow it isn't...

[RyanGlScott]

I now have a slightly better understanding on what is happening here. Here is a minimized example:

Definition F : bool -> Type -> Type :=
  fun b x =>
    if b then x else x.

Class Inhabited (a:Type) := MkInhabited { inhabitant : a }.

Global Hint Extern 5 (Inhabited ?A) =>
  (apply (@MkInhabited A); intuition (eauto with typeclass_instances inh)) : typeclass_instances.

Instance Inhabited_unit : Inhabited unit :=
  MkInhabited unit tt.

Instance Inhabited_F (b : bool) (a : Type) (Ha : Inhabited a) : Inhabited (F b a) :=
  MkInhabited
    (F b a)
    (match b with
     | true => inhabitant
     | false => inhabitant
     end).

Definition hm : forall (p : bool -> Type), forall {Inh_p : forall (_1 : bool), Inhabited (p _1)}, p true :=
  fun _ _ => inhabitant.

Definition onlyWorksOnOldCoq : unit :=
  hm (fun b : bool => F b unit).

onlyWorksOnOldCoq will typecheck with Coq 8.13 but not with Coq 8.14. I asked about this on the Coq Zulip chat here, and it was uncovered that Coq 8.14 is the only version in which this doesn't work, as there was a bug present in 8.14. Bummer. Besides 8.13, this also works with 8.15 and 8.16.

The nuclear option would be to give up on Coq 8.14 entirely. A slightly less extreme idea would be to tweak the way saw-core-coq handles Inhabited instance resolution. The issue lies with the Hint Extern declaration, which tries to automatically solve Inhabited instances for definitions that don't have explicit Instance declarations (e.g., PIntegral). At the same time, this Hint Extern isn't smart enough to solve for everything, so we must simultaneously be able to support hand-written instances for things that need them (e.g., the Inhabited (F b a) instance above).

Instead of relying on a Hint to accomplish automatic instance resolution, we could instead rely on a tactic. That is, we could do something like this:

Ltac inhabit :=
  apply @MkInhabited; intuition (eauto with typeclass_instances inh).

For most definitions, the inhabit tactic would be enough to implement an Inhabited instance without too much fuss:

Inductive Simple (b : bool) := MkSimple : Simple b.

Instance Inhabited_Simple (b : bool) : Inhabited (Simple b).
Proof. inhabit. Qed.

Definition test_Inhabited_Simple : Simple true :=
  hm (fun b : bool => Simple b).

Since much of saw-core-coq is autogenerated to begin with, we could also autogenerate the Instance declarations. For definitions where inhabit wouldn't suffice, we would have to wire up some special-casing to avoid generating Instance declarations and hand-write our own. (I'm unclear on how much work it would take to set up that special-casing.)

[eddywestbrook]

Well, yuck. It does seem kind of ridiculous to autogenerate instances just to support a single version of Coq, especially because there have been two major versions of Coq put out since then. It seems like we would do much better to put effort into supporting those newer versions of Coq, which we will want to do anyway at some point.

On that note, I tried to contact Anton Trunov, the maintainer of the coq-bits package, to ask if he plans to upgrade it to more recent versions of Coq, but I couldn't quite track down his contact info, though maybe I was too dumb to figure it out and someone else could give it a try? Otherwise, we could consider upgrading it ourselves, or maybe even writing our own version, since we have very specific needs and a strong dependency on it.

[RyanGlScott]

It seems like we would do much better to put effort into supporting those newer versions of Coq, which we will want to do anyway at some point.

I'm inclined to agree. I very briefly tried out my Ltac suggestion above, but it turns out to be much trickier to implement than what I suggested.

On that note, I tried to contact Anton Trunov, the maintainer of the coq-bits package, to ask if he plans to upgrade it to more recent versions of Coq, but I couldn't quite track down his contact info

I think this is his contact info: https://github.com/coq-community/bits/blob/734d8622b546fe4e99d47729d35cf82b591ef47e/coq-bits.opam#L5

[eddywestbrook]

Awesome, I knew you would be better at finding that contact info. I just sent Anton a note to ask about his intent with the Coq bits library.

[eddywestbrook]

I heard back from Anton Trunov, and he updated coq-bits to work with 8.15 and 8.16:

coq/opam#2332

Maybe we could see if the Coq extraction overall works with 8.15 now?

[RyanGlScott]

Thanks, @eddywestbrook!

saw-core-coq almost builds with Coq 8.15 and 8.16 save for one small issue: Coq 8.15 removes the deprecated Numeral Notation command in favor of Number Notation. As such, one has to apply the following patch to make saw-core-coq compile:

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
index a32846b4c..9b610324f 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
@@ -230,7 +230,7 @@ Definition sbvToInt (n : Nat) (b : bitvector n) : Z
 
 (* Useful notation for bools *)
 Definition boolToInt (b : bool) : Z := if b then 1%Z else 0%Z.
-Numeral Notation bool Z.odd boolToInt : bool_scope.
+Number Notation bool Z.odd boolToInt : bool_scope.
 Close Scope bool_scope. (* no, don't interpret all numbers as booleans... *)
 
 (* This is annoying to implement, so using BITS conversion *)

If I'm reading the 8.15 changelog correctly, Number Notation was introduced in Coq 8.13, so this change would effectively limit saw-core-coq's support back to 8.13. Is that a reasonable support window?