Permalink
Commits on Nov 16, 2018
  1. lib: fix up Levity dependency tracking

    Edward Pierzchalski
    Edward Pierzchalski committed Nov 13, 2018
    Uses proof body terms to disambiguate the names encoutered in
    dependency extraction, rather than using (for example)
    Thm.full_prop_of.
    
    The result is that this catches a few more missing dependencies,
    enough to correctly identify unused lemmas large sessions
    like CRefine.
Commits on Nov 15, 2018
  1. lib: an abbreviation command with pretty printing inside locales

    lsf37 and Xaphiosis committed Nov 15, 2018
    Normal abbreviations are not contracted on pretty printing when defined
    inside a locale. This commit provide the command locale_abbrev which does
    contract on pretty print even when defined inside a locale. It cannot be
    used with abbreviations that mention fixed locale variables (whereas the
    standard abbreviations can).
    
    Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Commits on Nov 6, 2018
Commits on Nov 2, 2018
  1. lib: fix up Levity JSON output

    Edward Pierzchalski
    Edward Pierzchalski committed Oct 22, 2018
    - Previously printed `~` for negative numbers, which is invalid
      JSON. Now prints `-`.
    
    - Previously the outpout would unconditionally trim
      'underscore-number' suffixes. Now uses theory context to determine
      if it's likely to be an index into a theory list or an existing
      fact name.
    
    - Changed JSON structure to avoid using dynamic names for keys, i.e.
      from this:
    
        {
          "my_theory_name": {...}
        }
    
      to this:
    
        {
          "theory": "my_theory_name",
          "content": {...}
        }
    
      This should make processing the output slightly nicer by matching
      what other tools expect.
    
    - Changed JSON structure to consolidate dependencies. Lemmas are no
      longer special-cased.
Commits on Oct 31, 2018
  1. access+infoflow+drefine: update for new definition of `idle_tcb_at`

    SantiagoBautista committed Oct 31, 2018
    * Context :
    
     We would like to prove that, for ARM_HYP architecture,
      the current vcpu is always the vcpu associated to the current thread.
     See issue https://jira.csiro.au/browse/VER-770
      and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291
    
     In this process, we changed the definition of `idle_tcb_at`
    
    * In this commit :
    
     Update some proofs in access, infoflow and drefine to take
      the new definition of `idle_tcb_at` into account.
  2. arm-hyp ainvs: prove that the vcpu of the idle thread is always None

    SantiagoBautista committed Oct 31, 2018
    * Context :
    
     We would like to prove that, for ARM_HYP architecture,
      the current vcpu is always the vcpu associated to the current thread.
     See issue https://jira.csiro.au/browse/VER-770
      and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291
    
    * Intermediate step : the vcpu of the idle thread is always None
    
     In this commit we update the proofs of abstract invariants for
      the arm_hyp architecture, so that the new version of `valid_idle`,
      stating that the vcpu of the idle thread is always None, holds.
  3. ainvs: changed definition of `valid_idle` + `idle_tcb_at` ; defined `…

    SantiagoBautista committed Oct 31, 2018
    …valid_arch_idle` invariant
    
    * Context :
    
     We would like to prove that, for ARM_HYP architecture,
     the current vcpu is always the vcpu associated to the current thread.
     See issue https://jira.csiro.au/browse/VER-770
     and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291
    
    * Intermediate step : the vcpu of the idle thread is always none
    
     In this commit, we modify the `valid_idle` invariant so that it includes
      the fact that the vcpu of the idle thread is always None.
     This is needed for PR291 (see Context above).
      `valid_idle` beeing defined with `idle_tcb_at`,
      we changed the definition of `idle_tcb_at`
      so that it can convey information about the architecture.
     And we defined `valid_arch_idle`
      that states that the vcpu of an iarch_tcb is None.
    
    * What changed :
    
     Even if these changes are only interesting for the
      abstract invariants for arm_hyp architecture
      (that are being extended),
      it implied changes to several generic and architecture-specific
      files of the astract invariants (AInvs) sessions.
    
    Co-authored-by : Corey Lewis <corey.lewis@data61.csiro.au>
    Co-authored-by : Santiago Bautista <santiago.bautista@data61.csiro.au>
Commits on Oct 25, 2018
  1. ainvs: clean up and arch split BCorres

    lsf37 committed Oct 11, 2018
    RISCV64 will need slight variations in the arch dependent proofs
  2. lib: clean up BCorres_UL

    lsf37 committed Oct 11, 2018
  3. lib: additional setup for numeral types

    lsf37 committed Oct 18, 2018
    In particular: instantiate to the size class so one can use bounded types
    for automatic termination measures in fun.
Commits on Oct 23, 2018
  1. lib/FastMap: add FIXME for conv_at hack

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 23, 2018
  2. lib: move FastMap lemma to LemmaBucket

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 23, 2018
  3. lib/FastMap: fix primrec style

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 16, 2018
  4. lib/FastMap: test cases for small inputs

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 16, 2018
  5. lib/FastMap: refactor convs; renaming; juggle function arguments

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 16, 2018
    Complex conversions have been refactored to the new utility conv_at,
    which is easier to use and has better error detection.
    
    Name changes: “*_to_map” naming scheme changed to more descriptive
    “*_to_lookup_list”.
    
    Key transformer argument is now the first argument to tree_lookup and
    friends, which matches functional programming conventions.
  6. lib/FastMap: use simple locale instead of unnecessary qualify

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 15, 2018
  7. lib: add FastMap tool

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 11, 2018
    Many issues remain (see TODO list), but it's now mature enough to be
    used for proof automation and has a comprehensive test suite.
  8. lib: remove reference to removed theories in ROOT

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 11, 2018
Commits on Oct 22, 2018
  1. test: allow CBaseRefine to run concurrently with Refine

    lsf37 committed Oct 16, 2018
    If Refine fails, it can still be useful to test CBaseRefine skipping over the
    failed Refine proofs (when that works).
  2. reduce DRefine dependencies from Refine to AInvs

    lsf37 committed Oct 13, 2018
    This needs (and includes) some deduplication and moving of lemmas formerly in
    refine.
Commits on Oct 10, 2018
  1. crefine: arm-hyp: add word lemma FIXMEs

    Edward Pierzchalski
    Edward Pierzchalski committed Sep 17, 2018
    Various potential improvements that became apparent during the word
    lemma move.
  2. Fix up proofs after word lemma moves

    Edward Pierzchalski
    Edward Pierzchalski committed Sep 17, 2018
  3. Remove pure word lemmas from proof/*

    Edward Pierzchalski
    Edward Pierzchalski committed Sep 20, 2018
    Removes redundant lemmas after moving them up to Word_Lib.
  4. lib: add some pure word lemmas found in proof/*

    Edward Pierzchalski
    Edward Pierzchalski committed Sep 17, 2018
    Preparation for removing duplicate word lemmas. These new lemmas
    don't belong in the AFP word library, so we hook in to
    `Word_Lemmas_Prefix` to expose them to our own theories.
  5. lib: speed up word8_exhaust

    Edward Pierzchalski
    Edward Pierzchalski committed Sep 17, 2018
Commits on Oct 3, 2018
  1. lib: bump LibTests timeout to 1800s

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 3, 2018
  2. lib: update qualified imports for LibTest theories

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 3, 2018
  3. run_tests: move selection of RefineOrphanage to run_tests

    Japheth Lim Japheth Lim
    Japheth Lim authored and Japheth Lim committed Oct 3, 2018
    This is more consistent with how we handle other broken proof sessions
    in the run_tests framework.