Skip to content
Formally verified implementation of Alive in Lean
Lean Other
  1. Lean 99.4%
  2. Other 0.6%
Branch: master
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.vscode
inputs/alive Initial commit Apr 27, 2018
src Remove TODOs, address the concerns at appropriate places Feb 7, 2019
.gitignore Initial commit Apr 27, 2018
LICENSE
README.md Remove deprecated scripts Feb 8, 2019
check_diff.py Update test scripts Feb 7, 2019
leanpkg.path
leanpkg.toml Update README.md, smt2_interface/mathlib commit id Feb 7, 2019
run-alive.sh Use xargs -0 instead of --null Apr 20, 2019
run-irtest.sh
run-proptest.sh Update test scripts Feb 7, 2019

README.md

AliveInLean

Setup

Run

# Run selected tests from Alive's test suite (which contain
# no precondition and do not require additional grammars)
./run-alive.sh
# Run random tests for the specification of Z3 expression -
# concrete value, as well as 4 admitted arithmetic lemmas.
# Note that bv_equiv.zext/sext/trunc will have 'omitted' tests
# because sometimes generated expressions try to compare
# bitvectors with different bitwidths.
./run-proptest.sh
# Run random tests for the specification of LLVM assembly language.
# Set clang path to yours by modifying the script.
./run-irtest.sh

Theorems

  • Specification, as well as proof, is in src/spec/.
  1. Execution of bigstep with two different value semantics (SMT expr / concrete value) has some good relations.
def encode (ss:irstate_smt) (se:irstate_exec) (η:freevar.env) :=
    irstate_equiv (η⟦ss⟧) se

def bigstep_both:= ∀ ss se (p:program) oss' ose' η
    (HENC:encode ss se η)
    (HOSS': oss' = bigstep irsem_smt ss p)
    (HOSE': ose' = bigstep irsem_exec se p),
  none_or_some oss' ose' (λ ss' se', encode ss' se' η)
-- Its proof is at equiv.lean
  1. We can generate initial state correctly.
def init_state_encode:= ∀ (freevars:list (string × ty)) (sg sg':std_gen) ise iss
    (HUNQ: list.unique $ freevars.map prod.fst)
    (HIE:(ise, sg') = create_init_state_exec freevars sg)
    (HIS:iss = create_init_state_smt freevars),
  ∃ η, encode iss ise η
-- Its proof is at initialstate.lean
  1. If refinement checking function check_single_reg0 says it's true, refinement indeed holds.
def refines_single_reg_correct := ∀ (psrc ptgt:program)
    (root:string) (ss0:irstate_smt) sb
    (HSREF:some sb = check_single_reg0 irsem_smt psrc ptgt root ss0)
    (HEQ:∀ (η0:freevar.env) e, b_equiv (η0⟦sb⟧) e → e = tt),
  root_refines_smt psrc ptgt ss0 root
-- Its proof is at refinement.lean

Contributing

This project welcomes contributions and suggestions. Most contributions require you to agree to a Contributor License Agreement (CLA) declaring that you have the right to, and actually do, grant us the rights to use your contribution. For details, visit https://cla.microsoft.com.

When you submit a pull request, a CLA-bot will automatically determine whether you need to provide a CLA and decorate the PR appropriately (e.g., label, comment). Simply follow the instructions provided by the bot. You will only need to do this once across all repos using our CLA.

This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact opencode@microsoft.com with any additional questions or comments.

You can’t perform that action at this time.