Skip to content
This repository has been archived by the owner on Dec 13, 2022. It is now read-only.

support for 8-bit and 16-bit MMIO #843

Merged
merged 11 commits into from
Jul 1, 2021
Merged

support for 8-bit and 16-bit MMIO #843

merged 11 commits into from
Jul 1, 2021

Commits on Jun 25, 2021

  1. wip adding support for 8bit MMIO 

    [does not compile yet]
    @samuelgruetter
    samuelgruetter committed Jun 25, 2021
    Configuration menu
    Copy the full SHA
    e09fae6 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2021

  1. wip, copy MinimalMMIO because incompatible with Kami/riscv-coq proof, 

    still doesn't compile, and access_size.word depending on machine width
and being the same as access_size.four in case of 32bit causes trouble
    @samuelgruetter
    samuelgruetter committed Jun 29, 2021
    Configuration menu
    Copy the full SHA
    08bbae9 View commit details
    Browse the repository at this point in the history

  2. update bedrock2 & coqutil to get better ZnWords

    @samuelgruetter
    samuelgruetter committed Jun 29, 2021
    Configuration menu
    Copy the full SHA
    77f025a View commit details
    Browse the repository at this point in the history

  3. using nat instead of access_size allows completing 

    StateMachineMMIO.compile_ext_call_correct, but the
files that need to satisfy the new assumptions of
StateMachineSemantics still don't work
    @samuelgruetter
    samuelgruetter committed Jun 29, 2021
    Configuration menu
    Copy the full SHA
    ad21488 View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2021

  1. update bedrock2 for better ZnWords

    @samuelgruetter
    samuelgruetter committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    2c50c0c View commit details
    Browse the repository at this point in the history

  2. prove that the Aes and Hmac state machine satisfy the new assumptions 

    of StateMachineSemantics, everything compiles again
    @samuelgruetter
    samuelgruetter committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    2dac80d View commit details
    Browse the repository at this point in the history

  3. make sure AesToC prelude uses the same MMIO names as the bedrock2 source

    @samuelgruetter
    samuelgruetter committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    727d485 View commit details
    Browse the repository at this point in the history

  4. fix outdated comments

    @samuelgruetter
    samuelgruetter committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    cd4ad9a View commit details
    Browse the repository at this point in the history

  5. Merge branch 'main' into 8bitMMIO

    @samuelgruetter
    samuelgruetter authored Jun 30, 2021
    Configuration menu
    Copy the full SHA
    a5e5788 View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2021

  1. style fix

    @samuelgruetter
    samuelgruetter committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    16da61e View commit details
    Browse the repository at this point in the history

  2. Merge branch '8bitMMIO' of github.com:samuelgruetter/silveroak into 8… 

    …bitMMIO
    @samuelgruetter
    samuelgruetter committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    fbe75f6 View commit details
    Browse the repository at this point in the history