coqutil

coqutil copied to clipboard

Bumps [etc/coq-scripts](https://github.com/JasonGross/coq-scripts) from `5876e80` to `857071d`. Commits 857071d Allow overriding sed and grep in reportify-coq-errors fb70f50 Compatibility with bash 3.x on Mac CI See full diff in compare view Dependabot...

dependabot[bot]

0adb

andres-erbsen

Merging fiat-crypto utilities into coqutil?

2

Should [any/all/most of the fiat-crypto `src/Util` directory](https://github.com/mit-plv/fiat-crypto/tree/master/src/Util) be migrated to coqutil? (Currently this directory is more-or-less replicated across fiat, rewriter, and fiat-crypto, with fiat-crypto containing the most complete and up-to-date...

JasonGross

hooking `word` into `lia`

1

Should https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2/ZnWords.v be adapted to hook into the zify mechanism a la https://github.com/coq/coq/blob/master/theories/micromega/ZifyUint63.v and be integrated into coqutil?

JasonGross

eradicating LittleEndian.combine

3

I have the feeling that using tuples in that file was an unfortunate choice and benefits almost nothing; getting rid of it would be a clear improvement. @samuelgruetter do you...

andres-erbsen

It would be better if coqutil used no axioms

5

coqchk gives: ``` CONTEXT SUMMARY =============== * Theory: Set is predicative * Axioms: Coq.ssr.ssrunder.Under_rel.Over_rel Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel Coq.ssr.ssrunder.Under_rel.over_rel Coq.Logic.FunctionalExtensionality.functional_extensionality_dep coqutil.Map.SortedList.TODO_andres Coq.ssr.ssrunder.Under_rel.over_rel_done Coq.ssr.ssrunder.Under_rel.Under_rel Coq.Logic.PropExtensionality.propositional_extensionality Coq.ssr.ssrunder.Under_rel.Under_relE coqutil.Map.SortedListString.TODO_andres Coq.ssr.ssrunder.Under_rel.under_rel_done * Constants/Inductives relying on type-in-type: *...

JasonGross

We can fix the first one with ```diff diff --git a/Makefile b/Makefile index d87b01a..a84f2b5 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,6 @@ default_target: all -.PHONY: clean force all install...

JasonGross

coqutil.Map.SortedListString.map cannot be extracted

5

This is currently blocking https://github.com/mit-plv/fiat-crypto/pull/686 (cc @jadephilipoom ) If I do ```coq Require Import Coq.extraction.Extraction. Require Import coqutil.Map.SortedListString. Extraction Language OCaml. Recursive Extraction coqutil.Map.SortedListString.map. ``` I get: ```ocaml type __...

JasonGross

Why is sextend a part of the word interface?

4

@samuelgruetter As sign extension goes from one word size to another word size, shouldn't it be a derived function from a word of one size to a word of another...

andres-erbsen-sifive