hax Coq proof lib

Add coq library files.

Dec 07 '23 13:12 cmester0

LGTM. Do we need MachineIntegers.v? The readme says to install it via opam.

Dec 07 '23 14:12 spitters

From what I can see MachineIntergers.v file is not directly part of CompCert library, so we do need it here.

Jan 06 '24 19:01 cmester0

From what I can see MachineIntergers.v file is not directly part of CompCert library, so we do need it here.

Interesting. So, where does it come from then? If possible, we should try to avoid code duplication.

Jan 07 '24 20:01 spitters

From what I can see MachineIntergers.v file is not directly part of CompCert library, so we do need it here.

Interesting. So, where does it come from then? If possible, we should try to avoid code duplication.

Hmm it might be here https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v , however it seems modifications been made to that file, as modules are used, while we just need a typeclass.

Jan 31 '24 17:01 cmester0

Yes, that seems like a likely source. It's possible that we are just using an old version. For the last yard, we've switched to the math-comp integers. It would be good to switch to the new stdlib one that's in preparation when it becomes available.

Jan 31 '24 20:01 spitters

Hi @cmester0, what's the status of this PR? seems to be mergeable, no?

Mar 07 '24 12:03 W95Psp

Yes, but I would like to add some testing, and structure the library a bit, but I guess those can be follow up PRs.

Mar 07 '24 13:03 cmester0

Why are you going back to the compcert integers? The jasmin/math-comp ones are needed for the jasmin connection.

Getting this merged would help us make a choice. Moreover, that library comes from fiat-crypto, which we also connect to with hacspec. https://github.com/coq/coq/pull/17043

Mar 25 '24 13:03 spitters

We have been using CompCert integers for the Coq backend, I was just updating them, to remove the weird extra file (MachineIntegers.v). If there is a better or more standard implementation, I can change the implementation to use that.

Mar 25 '24 14:03 cmester0

Ok. Yes, that's a good idea. Didn't we use the MC/jasmin integers for the SSProve backend?

On Mon, Mar 25, 2024 at 3:08 PM Lasse Letager Hansen < @.***> wrote:

We have been using CompCert integers for the Coq backend, I was just updating them, to remove the weird extra file (MachineIntegers.v). If there is a better or more standard implementation, I can change the implementation to use that.

— Reply to this email directly, view it on GitHub https://github.com/hacspec/hax/pull/386#issuecomment-2018089075, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTXNOFDWIZ3VX7GP6YTY2AVVPAVCNFSM6AAAAABALBNIJKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDAMJYGA4DSMBXGU . You are receiving this because your review was requested.Message ID: @.***>

Mar 25 '24 14:03 spitters

Converting this PR to a draft for now, @cmester0 can you undraft it whenever you want to merge it?

Apr 11 '24 11:04 W95Psp

This PR has been marked as stale due to a lack of activity for 60 days. If you believe this pull request is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

Oct 03 '24 02:10 github-actions[bot]

Closed in favor of #987 and annotated core lib.

Oct 10 '24 15:10 cmester0