Troubles getting cameleer to parse a file

[talex5]

I'm trying to use cameleer to verify https://github.com/ocaml-multicore/ocaml-uring/blob/main/lib/uring/heap.ml

It's a fairly simple data-structure that allocates numbered slots to callers (basically, it allows allocating and freeing unique IDs).

I'm having a hard time getting cameleer to parse it, though. Each time I try to simplify it a bit, I get another error. Here's the sequence I got:

Constants in case expressions are not supported.
File "../heap.ml", line 51, characters 26-34: Guarded expressions are not supported.
anomaly: "Assert_failure src/expression.ml:733:8"
File "../heap.ml", line 24, characters 0-110: Unbound type variable: 'b
File "../heap.ml", line 26, characters 4-9: Type symbol entry_rec expects 1 argument but is applied to 0
anomaly: Gospel.Uattr2spec.Syntax_error(_)
File "../heap.ml", line 51, characters 0-209: Symbol ptr is already defined in the current scope
File "../heap.ml", line 63, characters 40-44: unbound function or predicate symbol 'succ'
File "../heap.ml", line 68, characters 4-22: This application instantiates pure type variable 'a with a mutable type entry 'xi
anomaly: "Assert_failure src/expression.ml:733:8"
File "../heap.ml", line 68, characters 4-22: This application instantiates pure type variable 'a with a mutable type entry 'a
File "../heap.ml", line 68, characters 4-22: This application instantiates pure type variable 'a with a mutable type entry

Any suggestions on how to get it to accept this? I removed all the polymorphism by the end, so I don't know where it's getting the 'a from.

[mariojppereira]

How did you manage to go around the GADT for type 'a t definition? Can you provide the source code you are now trying to parse?

[talex5]

I just changed the extra_data field type to unit and made it a regular variant. That bit isn't important for the proof.

My attempts to fix it are here: https://github.com/talex5/ocaml-uring/commits/cameleer

Ideally though it would handle the original version.

[mariojppereira]

The error you get about instantiation of pure type variable is due to the fact that you are trying to build an array containing mutable elements. Why3 does not allow you to build such an array, i.e., the elements stored in an array cannot contain mutable fields (this would violate some of the memory static guarantees enforced by Why3).

In the particular case of your data structure, this happens since type entry is considered a mutable type, given the definition of entry_rec (mutable field ptr). When you call Array.make n Empty, the bad instantiation would occur.

I have pushed a new version of this implementation, accepted by Cameleer: mariojppereira/ocaml-uring@7475772

Please note there are also two other minor changes, due to namespace management:

1. Renamed the argument of alloc from data to entry_data
2. Renamed function in_use (bottom of the file) to in_use_

The latter happens since Why3 does not allow two symbols in the same namespace to have the same name (in_use is a field of a record type definition, which in Why3 is automatically converted into a global projection). The former, I am not so sure but it seems again to be some sort of clash between field names and local arguments (keeping the argument as data would cause an error when doing t.data.(ptr)). I will take a look into both issues to come up with a better name management system.

[talex5]

Ah, thanks. The ptr field does need to be mutable, since entry values are given to users and must be disabled when freed, but we can ignore that for now.

I still get an error though:

$ cameleer heap.ml
anomaly: Gospel.Uattr2spec.Syntax_error(_)

I also tried updating to the latest cameleer, but got Error: Unbound record field Uast.sp_header (I see the CI tests on master are failing with a similar-looking error: https://github.com/ocaml-gospel/cameleer/runs/3508158844)

[mariojppereira]

Sorry. There was an update on the GOSPEL side and forgot to update the cameleer.opam file. It should be fixed by now.

Any way to make this process more developer-friendly? Or does one really needs to update the pin-depends field each time a new commit arrives?

[talex5]

Well, something has to update if Cameleer changes to need a newer version of GOSPEL.

An alternative to pin-depends is to add it as a Git submodule. Then it's just a git pull in the submodule to update, and dune will build both projects as one. However, users often have problems with submodules (e.g. you have to clone with --recursive and remember to update submodules along with the main repository).

BTW, the current version still fails to build (Unbound module Location_error): https://github.com/ocaml-gospel/cameleer/runs/3525398068

[mariojppereira]

Sorry for the late response.

This should now be fixed in master.

[talex5]

Thanks - it parses now!