Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

crux-mir improvements for Ring verification #960

Open
wants to merge 13 commits into
base: master
Choose a base branch
from
Open

crux-mir improvements for Ring verification #960

wants to merge 13 commits into from

Commits on Apr 7, 2022

  1. crux-mir: add proc macro for defining MethodSpecs

    @spernsteiner
    spernsteiner committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    a4de54d View commit details
    Browse the repository at this point in the history

  2. crucible_spec_macro: various fixes for use with ring

    @spernsteiner
    spernsteiner committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    b6d0ab8 View commit details
    Browse the repository at this point in the history

  3. crux-mir: extend mem::transmute to handle int<->bytes

    @spernsteiner
    spernsteiner committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    e020622 View commit details
    Browse the repository at this point in the history

  4. update mir-json submodule

    @spernsteiner
    spernsteiner committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    497bf43 View commit details
    Browse the repository at this point in the history

Commits on Apr 8, 2022

  1. crux-mir: update golden test line numbers

    @spernsteiner
    spernsteiner committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    fa6b8e4 View commit details
    Browse the repository at this point in the history

Commits on Apr 18, 2022

  1. crux-mir: handle .dylib extension for libcrucible_spec_macro

    @spernsteiner
    spernsteiner committed Apr 18, 2022
    Configuration menu
    Copy the full SHA
    38fbbdc View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2022

  1. add a test for bswap

    @plredmond
    plredmond committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    091ecee View commit details
    Browse the repository at this point in the history

  2. add a stub implementation of a custom-translation for bswap, which im… 

    …plements the `id` function and therefore a wrong result
    @plredmond
    plredmond committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    d9e6875 View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2022

  1. incorrect implementation, but with a nice proof lol

    @plredmond
    plredmond committed Sep 1, 2022
    Configuration menu
    Copy the full SHA
    a3de070 View commit details
    Browse the repository at this point in the history

  2. fix the bswap implementation and proof; it's confusing because `BVSel… 

    …ect 0 ...` is LSB but the left argument to `BVConcat` is MSB

    impl 8   bv = bv
    impl bvw bv = let
        xsw = bvw - 8
        x  = BVSelect 0 8   bvw bv
        xs = BVSelect 8 xsw bvw bv
        in BVConcat 8 xsw x (impl xsw xs)
    @plredmond
    plredmond committed Sep 1, 2022
    Configuration menu
    Copy the full SHA
    08c4cec View commit details
    Browse the repository at this point in the history

  3. from_le_bytes and from_be_bytes tests for more word widths

    @plredmond
    plredmond committed Sep 1, 2022
    Configuration menu
    Copy the full SHA
    30a80a6 View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2022

  1. separate proof from implementation in the bswap custom implementation

    @plredmond
    plredmond committed Sep 14, 2022
    Configuration menu
    Copy the full SHA
    ed4a36e View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2022

  1. Merge pull request #1038 from plredmond/crux-mir_bswap 

    [crux-mir] Implement bswap intrinsic
    @spernsteiner
    spernsteiner committed Oct 21, 2022
    Configuration menu
    Copy the full SHA
    a8b1be1 View commit details
    Browse the repository at this point in the history