Issues with VST Installation via OPAM (coq-vst.3.0beta2)

[laforetbarroso]

I’ve recently installed the VST on Iris via OPAM using the package coq-vst.3.0beta2. While working on specifying a simple program, I encountered the following issue related to unresolved implicit arguments:

The following term contains unresolved implicit arguments:
  (ident * funspec)%type
More precisely: 
- ?Σ: Cannot infer the implicit parameter Σ of funspec whose type is "gFunctors".

Additionally, when attempting to run the example verification files (such as verif_reverse.v), I’m running into issues importing VST.floyd.compat.

[mansky1]

Thank you for trying out VST 3.0!

1. In your simple example, are you working in a context with a Σ (e.g., Context {!VSTGS OK_ty Σ})? Also, does this error go away if you simply remove the type annotation? If the answers are "yes" and "no", please show more of the file (or email me at mansky1@uic.edu) and I can debug further.
2. What's the error message with floyd.compat? Is it simply not present/not installed?

[mansky1]

Actually, the floyd.compat issue is a known problem that we fixed a couple days afterwards, but haven't patched in OPAM. You can either compile it manually (e.g., go into your opam VST installation and run coqc -Q floyd VST.floyd floyd/compat.v) or wait for the release of 3.1beta (hopefully in the next week or so).

[laforetbarroso]

Thank you for trying out VST 3.0!

1. In your simple example, are you working in a context with a Σ (e.g., Context {!VSTGS OK_ty Σ})? Also, does this error go away if you simply remove the type annotation? If the answers are "yes" and "no", please show more of the file (or email me at mansky1@uic.edu) and I can debug further.
2. What's the error message with floyd.compat? Is it simply not present/not installed?

I'm not working in a context with a Σ, and the error persists even after removing the type annotation.

To clarify the issue and rule out any mistakes on my part, I did the following:

1. Copied the odd.c file from the examples
2. Ran clightgen -normalize odd.c
3. Used coqc to compile odd.v
4. Tried to define a specification for odd using the following definition:

Require Import VST.floyd.proofauto.
Require Import GC.odd.

#[export] Instance CompSpecs : compspecs.
Proof. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Local Open Scope assert.

Definition odd_spec :=
 DECLARE _odd
  WITH z : Z, b: unit
  PRE [ tuint]
    PROP(0 <= z <= Int.max_signed) PARAMS(Vint (Int.repr z)) SEP()
  POST [ tint ]
    PROP() RETURN(Vint (if Z.odd z then Int.one else Int.zero)) SEP().

However, still gives the following error:

The following term contains unresolved implicit arguments:
  (_odd : ident,
(WITH x : Z * () PRE
[tuint] (let (z, _) := x in
PROP (0 <= z <= Int.max_signed) PARAMS (Vint (Int.repr z)) SEP ())
POST [tint] (let (z, _) := x in
PROP ( ) RETURN (Vint (if Z.odd z then Int.one else Int.zero)) SEP ()))
:
funspec)
More precisely: 
- ?Σ: Cannot infer the implicit parameter Σ of funspec whose type is "gFunctors".

[laforetbarroso]

Actually, the floyd.compat issue is a known problem that we fixed a couple days afterwards, but haven't patched in OPAM. You can either compile it manually (e.g., go into your opam VST installation and run coqc -Q floyd VST.floyd floyd/compat.v) or wait for the release of 3.1beta (hopefully in the next week or so).

Thanks for the info! That makes sense. I’ll try compiling compat.v manually for now and keep an eye out for the 3.1 beta release.

[mansky1]

Okay, I see the problem with the funspec type. First, if you're not planning to use Iris-style features, you should Require Import VST.floyd.compat; otherwise, you have to add some boilerplate (specifically, start a section with Context {!VSTGS OK_ty Σ} in it) before you write any funspecs. Second, there's an annoying type inference issue for specs that don't have any memory assertions; once you've imported compat, adding the type annotation : ident * funspec to odd_spec should fix it.

[laforetbarroso]

Thanks, that clears it up! After importing VST.floyd.compat and adding the type annotation : ident * funspec to odd_spec, it works fine now. I really appreciate the help!