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

Compiler correctness for Armv8 built on an official specification #858

Merged
merged 6 commits into from
Feb 11, 2022
Merged

Compiler correctness for Armv8 built on an official specification #858

merged 6 commits into from
Feb 11, 2022

Commits on Dec 1, 2021

  1. Sketch out proofs of compile_correct for ASL-derived Armv8

    @hrutvik
    hrutvik committed Dec 1, 2021
    Configuration menu
    Copy the full SHA
    566c343 View commit details
    Browse the repository at this point in the history

Commits on Dec 2, 2021

  1. Factor some tactics/lemmas out of arm8_targetProofTheory into a lib… 

    …rary
    @hrutvik
    hrutvik committed Dec 2, 2021
    Configuration menu
    Copy the full SHA
    49546c7 View commit details
    Browse the repository at this point in the history

Commits on Dec 7, 2021

  1. Prove encoder_correct for ASL-derived Armv8 

    This proof could do with streamlining - it is considerably slower and more
verbose than the L3 proofs
    @hrutvik
    hrutvik committed Dec 7, 2021
    Configuration menu
    Copy the full SHA
    8db3046 View commit details
    Browse the repository at this point in the history

  2. Add ASL-derived Armv8 to build sequence

    @hrutvik
    hrutvik committed Dec 7, 2021
    Configuration menu
    Copy the full SHA
    02c1a55 View commit details
    Browse the repository at this point in the history

Commits on Jan 21, 2022

  1. Merge remote-tracking branch 'origin/master' into asl-equiv

    @hrutvik
    hrutvik committed Jan 21, 2022
    Configuration menu
    Copy the full SHA
    1b5c048 View commit details
    Browse the repository at this point in the history

Commits on Jan 25, 2022

  1. Delay building of L3 equivalence proofs until needed

    @hrutvik
    hrutvik committed Jan 25, 2022
    Configuration menu
    Copy the full SHA
    874bb72 View commit details
    Browse the repository at this point in the history