Code

Rules for Lib#704

Code

Merged

michaelmcinerney merged 21 commits intomasterseL4/l4v:masterfrom michaelm-rules_for_LibseL4/l4v:michaelm-rules_for_LibCopy head branch name to clipboardJan 15, 2024

+717-99

Commits

Commits on Jan 15, 2024

• lib+refine: strengthen corres_assert_assume_l and move to Lib

  Show description for e4ec9f3
  michaelmcinerney

  committed
  e4ec9f3

• lib: add corres_if_strong

  Show description for ca3624e
  michaelmcinerney

  committed
  ca3624e

• lib: add some rules involving ex_abs_underlying, including corres_from_valid

  Show description for 45ece43
  michaelmcinerney

  committed
  45ece43

• lib: strengthen no_ofail_gets_the

  Show description for 48f8ea7
  michaelmcinerney

  committed
  48f8ea7

• lib: add monadic_rewrite_guard_arg_cong

  Show description for d13c538
  michaelmcinerney

  committed
  d13c538

• lib: generalise monadic_rewrite_is_valid

  Show description for 0078984
  michaelmcinerney

  committed
  0078984

• lib: add monadic_rewrite_corres_r_generic_ex_abs

  Show description for 25968fd
  michaelmcinerney

  committed
  25968fd

• lib: add ifM_to_top_of_bind

  Show description for 962d097
  michaelmcinerney

  committed
  962d097

• lib: add ifM_corres' and orM_corres'

  Show description for f2b047f
  michaelmcinerney

  committed
  f2b047f

• lib: reorder assumptions of no_fail_bind

  Show description for 4edbe22
  michaelmcinerney

  committed
  4edbe22

• lib: modify no_ofail_obind and no_ofail_pre_imp

  Show description for 04e7eea
  michaelmcinerney

  committed
  04e7eea

• lib: add ovalid_post_taut

  Show description for 943ab13
  michaelmcinerney

  committed
  943ab13

• lib: add no_ofail_if

  Show description for 82abdf8
  michaelmcinerney

  committed
  82abdf8

• lib: add defn of list_insert_before, and some lemmas

  Show description for c486058
  michaelmcinerney

  committed
  c486058

• lib: add Heap_List.thy, for reasoning about linked lists on heaps

  Show description for fd6656c
  michaelmcinerney

  committed
  fd6656c

• lib: heap_ls lemmas relating an update to the list to an update to the heap

  Show description for 0f5987a
  michaelmcinerney

  committed
  0f5987a

• lib: add heap_path_sym_heap_non_nil_lookup_prev

  Show description for b2962e9
  michaelmcinerney

  committed
  b2962e9

• lib: add fun_upd_swap

  Show description for d04daa5
  michaelmcinerney

  committed
  d04daa5

• lib: several miscellaneous lemmas for heap_ls

  Show description for d588c6c
  michaelmcinerney

  committed
  d588c6c

• lib: add "no loops" lemmas for heap_ls

  Show description for 1991f59
  michaelmcinerney

  committed
  1991f59

• lib: some sym_heap lemmas regarding heap updates

  Show description for 58d5752
  michaelmcinerney

  committed
  58d5752