Coq proof lib #386
Coq proof lib #386
Conversation
|
LGTM. Do we need MachineIntegers.v? The readme says to install it via opam. |
|
From what I can see |
| From Hacspec Require Export MachineIntegers. | ||
| From Hacspec Require Export Hacspec_Lib. | ||
|
|
||
| (** Should be moved to Hacspec_Lib.v **) |
proof-libs/coq/coq/src/Hacspec_lib.v
Outdated
| Notation get_exact_chunk := seq_get_exact_chunk. | ||
| Definition set_chunk {a: Type} `{Default a} {len} (s: seq a) {WS} (chunk_len: @int WS) (chunk_num: @int WS) (chunk: array_or_seq a len) : seq a := seq_set_chunk s (unsigned chunk_len) (unsigned chunk_num) (as_seq chunk). | ||
| Definition set_exact_chunk {a} `{H : Default a} {len} s {WS} := @set_chunk a H len s WS. | ||
| Notation get_remainder_chunk := seq_get_remainder_chunk. |
| end). | ||
| Definition g_public_byte_seq : G (public_byte_seq) := | ||
| listOf arbitrary. | ||
| (* @genList int8 gen_int8. *) |
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. |
|
Yes, that seems like a likely source. |
|
Hi @cmester0, what's the status of this PR? seems to be mergeable, no? |
|
Yes, but I would like to add some testing, and structure the library a bit, but I guess those can be follow up PRs. |
|
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. |
|
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. |
|
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
<#386 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AABTNTXNOFDWIZ3VX7GP6YTY2AVVPAVCNFSM6AAAAABALBNIJKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDAMJYGA4DSMBXGU>
.
You are receiving this because your review was requested.Message ID:
***@***.***>
|
cmester0
force-pushed
the
coq_lib
branch
2 times, most recently
from
7fde53b
to
d2fbf65
Compare
Pull request was converted to draft
|
Converting this PR to a draft for now, @cmester0 can you undraft it whenever you want to merge it? |
|
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. |
|
Closed in favor of #987 and annotated core lib. |
Add coq library files.