search

AU-COBRA / ConCert

A framework for smart contract verification in Coq
MIT License
114 stars 19 forks source link

Update to MetaCoq 1.3 #242

Open womeier opened 6 months ago

womeier commented 6 months ago

I was looking into extracting the counter module to concordium, using our Wasm backend for CertiCoq.

CertiCoq is currently on MetaCoq 1.3, which ConCert doesn't seem to work with.

Do you already have plans to update?

4ever2 commented 6 months ago

I already started looking at updating to MetaCoq 1.3. However, I ran into a problem that looks like a MetaCoq bug. I haven't had time yet to identify the exact cause of the problem.

spitters commented 6 months ago

@4ever2 we should get ConCert in MetaCoq CI...

spitters commented 6 months ago

Here's what we need to do. Let's find a local Nix expert... https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/CI/near/292131799

On Tue, Apr 9, 2024 at 9:17 AM 4ever2 @.***> wrote:

I already started looking at updating to MetaCoq 1.3. However, I ran into a problem that looks like a MetaCoq bug. I haven't had time yet to identify the exact cause of the problem.

— Reply to this email directly, view it on GitHub https://github.com/AU-COBRA/ConCert/issues/242#issuecomment-2044301831, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTWJTB7EYBW2QDIDETTY4OI2FAVCNFSM6AAAAABF54QKOOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANBUGMYDCOBTGE . You are receiving this because you are subscribed to this thread.Message ID: @.***>

womeier commented 6 months ago

I already started looking at updating to MetaCoq 1.3. However, I ran into a problem that looks like a MetaCoq bug. I haven't had time yet to identify the exact cause of the problem.

@4ever2 It seems you have a version that works with MC 1.3 (without support for the elm extraction, that's no big deal of course). Could you push that to a branch? Things break at various places when I update to MC 1.3.

womeier commented 6 months ago

I have a version of ConCert now (with a bunch of things commented out), that compiles with MetaCoq 1.3.

Extracting the counter smart contract works, but I can't yet compile the extracted rust project as I'm not sure how to set up the required concordium libraries. Could you give me a pointer on which versions of which packages I should install?

Running cargo build in extraction/tests/extracted-code/concordium-extract/counter-extracted gives the following error:

error: failed to select a version for the requirement `concordium-std-derive = "^2.0"`
candidate versions found which didn't match: 6.0.0
location searched: crates.io index
required by package `concordium-std v2.0.0`
    ... which satisfies dependency `concordium-std = "^2.0.0"` of package `concert-std v0.1.0 (/home/wolfgang/ProjectsUni/Compilerstep/smart_contracts/ConCert/extraction/tests/extracted-code/concordium-extract/concert-std)`

It seems I need version 2.0.0, which is not available via crates.io, is that what you currently use?

spitters commented 4 months ago

@womeier I seem to recall you made progress on this. What's the current status?

womeier commented 4 months ago

I commented out some proofs and tests, to make the counter module extraction work with MetaCoq 1.3, I don't think the other smart contracts work.

These are my changes: https://github.com/womeier/coq-rust-extraction/commit/f113dff206a58eb508213eb0e46aaf9695205baa https://github.com/womeier/ConCert/commit/cf5d7d80a358ad1c50d564c67c20c312ac2f5d4f