How to fix coq error in riscv_duopod?

[nazar-codethink]

I'm trying to compile riscv_duopod with coqc and getting the following error:

Unable to solve constraint
width : Z
addr : (mword 64)
Goal: (0 <= width)
Unable to solve constraint
width : Z
addr : (mword 64)
Goal: (0 <= width)
File "./out.v", line 79, characters 0-173:
Error:
The following term contains unresolved implicit arguments:
  (fun (addr : mword 64) (width : Z) =>
   MEMr 64 width
     (EXTZ 64
        ((MachineWord.MachineWord.N_to_word (Pos.to_nat 4)
            (HexString.Raw.to_N "0" 0)
          :
          mword 4)
         :
         mword 4)) addr
   :
   M (mword (8 * width)))
More precisely: 
- ?H: Cannot infer the implicit parameter H of MEMr whose type is
  "ArithFact (width >=? 0)" (no type class instance found) in
  environment:
  addr : mword 64
  width : Z

I have installed sail 0.16, coq-sail 0.16, coq 8.16.1, coq-bbv 1.3. I generated out.v and out_types.v from riscv_duopod.sail, and I copied riscv_extras.v and mem_metadata.v from sail-riscv repository. Then I added Require Import mem_metadata. Require Import riscv_extras. to out.v and tried to compile them with coqc. What am I doing wrong here?

Here's all 4 files: riscv_duopod.zip

[Alasdair]

I'm not sure what the solution to this, our main Sail to Coq expert is away on Holiday right now, so apologies if it takes a while to get a good answer to this.

[bacam]

The Coq target for the main RISC-V needs to be updated, which is causing the problem that you're seeing. Instead, add a file called riscv_duopod_extras.v containing

From Sail Require Import Base.

Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize) : monad rv (mword (8 * size)) e := read_mem Read_plain addrsize addr size.

and build it all using

sail -coq -coq_lib riscv_duopod_extras -o riscv_duopod riscv_duopod.sail
coqc riscv_duopod_extras.v
coqc riscv_duopod_types.v
coqc riscv_duopod.v

and it should work.

I'll add this to the Sail repository soon, and later update the main Sail RISC-V definitions.