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:
***@***.***>
|
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? |
Add coq library files.