mit-plv/fiat-crypto issues and pull requests

#1855 - Bench garagedoor april2

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1853 - [DO NOT MERGE] Bench garagedoor april

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1852 - move only_mmio_satisfying to bedrock2

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1851 - Bump rupicola from `e849928` to `d9d95af`

Pull Request - State: closed - Opened by dependabot[bot] 6 months ago - 1 comment
Labels: submodules

#1850 - Bump rupicola from `2aa6b13` to `e849928`

Pull Request - State: closed - Opened by dependabot[bot] 6 months ago - 2 comments
Labels: submodules

#1849 - paperify spec

Pull Request - State: closed - Opened by andres-erbsen 6 months ago - 1 comment

#1848 - Decide point equality

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1847 - instantiate Edwards-Montgomery isomorphism for Curve25519

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1846 - bump bedrock2, use "always" in GarageDoor spec

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1845 - implement and prove Curve25519 scalar clamping

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1844 - Edwards twist isomorphism

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1843 - merge Group.Scalarmult into MontgomeryLadder, use in x25519_base

Pull Request - State: closed - Opened by andres-erbsen 6 months ago

#1842 - Update coq-docker.yml: Bump binaryen vesion

Pull Request - State: closed - Opened by JasonGross 6 months ago

#1841 - merge MontgomeryEquivalence into MontgomeryLadder

Pull Request - State: closed - Opened by andres-erbsen 6 months ago - 2 comments

#1840 - Bump rewriter from `21b82e9` to `1cd64f2`

Pull Request - State: closed - Opened by dependabot[bot] 6 months ago
Labels: submodules

#1839 - Rust Crate Version Bump

Pull Request - State: closed - Opened by github-actions[bot] 7 months ago
Labels: rust, automated pr

#1838 - Use etc/ci/github-actions-make.sh on alpine

Pull Request - State: closed - Opened by JasonGross 7 months ago - 1 comment

#1837 - Slow BarrettReduction?

Issue - State: open - Opened by JasonGross 7 months ago

#1836 - Bump actions/setup-java from 4.1.0 to 4.2.1

Pull Request - State: closed - Opened by dependabot[bot] 7 months ago
Labels: dependencies

#1835 - Bump rupicola from `e047275` to `7259f52`

Pull Request - State: closed - Opened by dependabot[bot] 7 months ago - 2 comments
Labels: submodules

#1834 - [do not merge] bench garagedoor build with -j on Arch

Pull Request - State: closed - Opened by andres-erbsen 7 months ago

#1833 - [do not merge] bench garagedoor build on arch

Pull Request - State: closed - Opened by andres-erbsen 7 months ago

#1832 - [do not merge] Time garagedoor build

Pull Request - State: closed - Opened by andres-erbsen 7 months ago

#1831 - Please create a tag for Coq 8.19 in Coq Platform 2024.01

Issue - State: closed - Opened by rtetley 7 months ago - 15 comments

#1830 - Adapt definitional classes to coq/coq#18590

Pull Request - State: closed - Opened by JasonGross 7 months ago

#1829 - Bump etc/coq-scripts from `7b54b75` to `5876e80`

Pull Request - State: closed - Opened by dependabot[bot] 7 months ago
Labels: submodules

#1828 - Bump etc/coq-scripts from `7b54b75` to `5876e80`

Pull Request - State: closed - Opened by dependabot[bot] 7 months ago
Labels: submodules, sp2019latest

#1827 - [sp2019latest] Adapt to coq/coq#18590

Pull Request - State: closed - Opened by JasonGross 7 months ago

#1826 - adapt to coq/coq#18730

Pull Request - State: closed - Opened by andres-erbsen 7 months ago

#1825 - Bump bbv from `f4caa05` to `c53d5b9`

Pull Request - State: closed - Opened by dependabot[bot] 7 months ago
Labels: submodules, sp2019latest

#1824 - Bump actions/setup-java from 4.0.0 to 4.1.0

Pull Request - State: closed - Opened by dependabot[bot] 7 months ago - 1 comment
Labels: dependencies

#1823 - Joye double-add ladder for short Weierstrass curves in co-Z arithmetic

Pull Request - State: closed - Opened by atrieu 7 months ago - 7 comments

#1822 - Change fiat_25519_opp to return a tight?

Issue - State: closed - Opened by 0x0ece 7 months ago - 1 comment

#1821 - Adapt to https://github.com/coq/coq/pull/18590

Pull Request - State: closed - Opened by proux01 8 months ago

#1820 - Mask most significant bit in from_bytes

Issue - State: open - Opened by 0x0ece 8 months ago - 2 comments

#1819 - Bump rewriter from `3342e29` to `21b82e9`

Pull Request - State: closed - Opened by dependabot[bot] 8 months ago
Labels: submodules

#1818 - bump rupicola (requires Coq >= 8.18)

Pull Request - State: closed - Opened by samuelgruetter 8 months ago

#1817 - Rust Crate Version Bump

Pull Request - State: closed - Opened by github-actions[bot] 8 months ago
Labels: rust, automated pr

#1816 - Bump peter-evans/create-pull-request from 5 to 6

Pull Request - State: closed - Opened by dependabot[bot] 8 months ago
Labels: dependencies

#1815 - Bump rewriter from `ff800d3` to `3342e29`

Pull Request - State: closed - Opened by dependabot[bot] 8 months ago
Labels: submodules

#1814 - adapt to coq/coq#18563

Pull Request - State: closed - Opened by andres-erbsen 8 months ago

#1813 - Bump rewriter from `de9f96d` to `9e81a52`

Pull Request - State: closed - Opened by dependabot[bot] 8 months ago - 1 comment
Labels: submodules

#1812 - adapt to coq/coq#18563

Pull Request - State: closed - Opened by andres-erbsen 8 months ago

#1811 - Bump rupicola from `90a9655` to `9f17f7c`

Pull Request - State: closed - Opened by dependabot[bot] 8 months ago
Labels: submodules

#1810 - Bump ammaraskar/gcc-problem-matcher from 0.2.0 to 0.3.0

Pull Request - State: closed - Opened by dependabot[bot] 8 months ago
Labels: dependencies

#1809 - Fix DCE/Subst01 to work under lambdas

Pull Request - State: closed - Opened by JasonGross 8 months ago

#1808 - Cache intermediate values for Edwards addition

Pull Request - State: closed - Opened by bMacSwigg 9 months ago

#1807 - Adapt to Coq's PR #18445 fixing inheritance of multiple signatures of implicit arguments in notations

Pull Request - State: closed - Opened by herbelin 9 months ago - 1 comment

#1806 - [CI] [ArchLinux] Update keys

Pull Request - State: closed - Opened by JasonGross 9 months ago - 1 comment

#1805 - Bump rewriter from `c0328db` to `de9f96d`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago - 1 comment
Labels: submodules

#1804 - Fix nested unordered lists in README.md

Pull Request - State: closed - Opened by divergentdave 9 months ago

#1803 - Add ArchLinux CI badge to README

Pull Request - State: closed - Opened by JasonGross 9 months ago

#1802 - Downgrade actions/{download,upload}-artifact 4=>3

Pull Request - State: closed - Opened by JasonGross 9 months ago

#1801 - Revert "Bump actions/download-artifact and actions/upload-artifact from 3 to 4 (#1786)"

Pull Request - State: closed - Opened by JasonGross 9 months ago

#1800 - Bump etc/coq-scripts from `d3dc888` to `7b54b75`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago
Labels: submodules, sp2019latest

#1799 - Bump rewriter from `0388980` to `c0328db`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago
Labels: submodules

#1798 - Unify Coq CI into a single .yml file

Pull Request - State: open - Opened by JasonGross 9 months ago - 2 comments

#1797 - [CI] Drop Arch Linux workaround

Pull Request - State: open - Opened by JasonGross 9 months ago
Labels: awaiting-merge-of-dependency

#1796 - [CI] Drop alpine workaround

Pull Request - State: closed - Opened by JasonGross 9 months ago

#1795 - Bump rewriter from `f7e3fe5` to `0388980`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago - 1 comment
Labels: submodules

#1794 - Bump etc/coq-scripts from `d3dc888` to `7b54b75`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago - 1 comment
Labels: submodules

#1793 - [ci] [alpine] Use --root instead of sudo

Pull Request - State: closed - Opened by JasonGross 9 months ago - 1 comment

#1792 - Bump rewriter from `4bece97` to `f7e3fe5`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago - 1 comment
Labels: submodules

#1791 - Bump rewriter from `90549d8` to `4bece97`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago - 2 comments
Labels: submodules

#1790 - Bump rewriter from `90549d8` to `604362b`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago - 2 comments
Labels: submodules

#1789 - Bump rewriter from `90549d8` to `44552d2`

Pull Request - State: closed - Opened by dependabot[bot] 9 months ago - 3 comments
Labels: submodules

#1788 - [CI] Add Arch Linux test

Pull Request - State: closed - Opened by JasonGross 9 months ago - 1 comment

#1787 - Installation problems on Arch Linux: Package `coq-core.plugins.ltac' not found

Issue - State: closed - Opened by defeo 10 months ago - 5 comments

#1786 - Bump actions/download-artifact and actions/upload-artifact from 3 to 4

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1785 - Bump actions/download-artifact from 3 to 4

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago - 3 comments
Labels: dependencies

#1784 - Bump actions/upload-artifact from 3 to 4

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago - 3 comments
Labels: dependencies

#1783 - Augment rewrite rule proving tactics for saturated arithmetic

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1782 - Bump rewriter from `22162aa` to `90549d8`

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago
Labels: submodules

#1781 - Bump rewriter from `3a0a5f7` to `22162aa`

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago - 2 comments
Labels: submodules

#1780 - Add prod_rect rewrite rule for saturated arithmetic

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1779 - Allow leaving over shelved goals when debugging cache_term

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1778 - Add remaining rewrite rules for saturated arithmetic

Pull Request - State: open - Opened by JasonGross 10 months ago - 6 comments

#1777 - Unobjectionable rewrite rules for saturated arithmetic

Pull Request - State: open - Opened by JasonGross 10 months ago - 1 comment
Labels: needs: fixing

#1776 - Bump rewriter from `026f87b` to `3a0a5f7`

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago
Labels: submodules

#1775 - Add `subst!` and `typeof!` to `Notations.v`

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1774 - Add remaining identifiers for saturated solinas

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1773 - Add more identifiers for saturated solinas

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1772 - Bump actions/setup-go from 4 to 5

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago
Labels: dependencies

#1771 - Bump actions/setup-python from 4 to 5

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago
Labels: dependencies

#1770 - Add support for applying bool functions to zrange

Pull Request - State: closed - Opened by JasonGross 10 months ago - 1 comment

#1769 - More fine-grained bounds analysis

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1768 - Add `Util.Option.bind2`

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1767 - Update ZRangeProofs

Pull Request - State: closed - Opened by JasonGross 10 months ago
Labels: awaiting-merge-of-dependency

#1766 - Add some more ZRangeProofs

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1765 - Bump rewriter from `c45abd0` to `026f87b`

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago
Labels: submodules

#1764 - Factor ZRange Proper proof

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1763 - Bump rewriter from `bf64674` to `c45abd0`

Pull Request - State: closed - Opened by dependabot[bot] 10 months ago
Labels: submodules

#1762 - Future-proof CompilersTestCases

Pull Request - State: closed - Opened by JasonGross 10 months ago

#1761 - Don't replace abstract state of higher order functions with `bottom` when we can avoid it (now guarded by `--fancy-and-powerful-but-exponentially-slow-bounds-analysis`)

Pull Request - State: open - Opened by JasonGross 10 months ago - 4 comments

GitHub / mit-plv/fiat-crypto issues and pull requests