GitLab

simplify_equality        => simplify_eq
simplify_equality'       => simplify_eq/=
simplify_map_equality    => simplify_map_eq
simplify_map_equality'   => simplify_map_eq/=
simplify_option_equality => simplify_option_eq
simplify_list_equality   => simplify_list_eq
f_equal'                 => f_equal/=

The /= suffixes (meaning: do simpl) are inspired by ssreflect.

The singleton maps notation is now also more consistent with the
insert <[_ := _]> _ notation for maps.

Also, make our redefinition of done more robust under different
orders of Importing modules.

Also do some minor clean up.

Important changes in the core semantics:
* Types extended with function types. Since function types are a special kind
  of pointer types, types now have an additional mutual part called "ptr_type".
* Pointers extended with function pointers. Theses are just names that refer
  to an actual function in the function environment.
* Typing environments extended to assign argument and return types to function
  names. Before we used a separate environment for these, but since the
  argument and return types are already needed to type function pointers, this
  environment would appear in pretty much every typing judgment.

As a side-effect, the frontend has been rewritten entirely. The important
changes are:

* Type checking of expressions is more involved: there is a special kind of
  expression type corresponding to a function designator.
* To handle things like block scoped extern function, more state-fullness was
  needed. To prepare for future extensions, the entire frontend now uses a
  state monad.

Integers with the same size, are no longer supposed to have the same rank. As a
result, the C integer types (char, short, int, long, long long) are different
(and thus cannot alias) even if they have the same size. We now have to use a
more involved definition of integer promotions and usual arithmetic conversions.
However, this new definition follows the C standard literally.

The proof now uses the stronger notion of memory permutation instead of a more
general memory refinement. We have also proven that memory permutations are
symmetric.

Now it only performs injection on hypotheses of the shape f .. = f ..

memory instead of the whole memory itself.

This has the following advantages:
* Avoid parametrization in {addresses,pointers,pointer_bits,bits}.v
* Make {base_values,values}.v independent of the memory, this makes better
  parallelized compilation possible.
* Allow small memories (e.g. singletons as used in separation logic) with
  addresses to objects in another part to be typed.
* Some proofs become easier, because the memory environments are preserved
  under many operations (insert, force, lock, unlock).

It also as the following disadvantages:
* At all kinds of places we now have explicit casts from memories to memory
  environments. This is kind of ugly. Note, we cannot declare memenv_of as a
  Coercion because it is non-uniform.
* It is a bit inefficient with respect to the interpreter, because memory
  environments are finite functions instead of proper functions, so calling
  memenv_of often (which we do) is not too good.

Major changes:
* Make void a base type, and include a proper void base value. This is necessary
  because expressions (free, functions without return value) can yield a void.
  We now also allow void casts conforming to the C standard.
* Various missing lemmas about typing, weakening, decidability, ...
* The operations "free" and "alloc" now operate on l-values instead of r-values.
  This removes some duplication.
* Improve notations of expressions and statements. Change the presence of the
  operators conforming to the C standard.

Small changes:
* Use the classes "Typed" and "TypeCheck" for validity of indexes in memory.
  This gives more uniform notations.
* New tactic "typed_inversion" performs inversion on an inductive predicate
  of type "Typed" and folds the premises.
* Remove a horrible hack in the definitions of the classes "FMap", "MBind",
  "OMap", "Alter" that was used to let "simpl" behave better. Instead, we have
  defined a tactic "csimpl" that folds the results after performing an
  ordinary "simpl".
* Fast operation to remove duplicates from lists using hashsets.
* Make various type constructors (mainly finite map implementations) universe
  polymorphic by packing them into an inductive. This way, the whole C syntax
  can live in type, avoiding the need for (slow) universe checks.

Major changes:
* A data structure to collect locked addresses in memory.
* Operations to lock and unlock addresses.
* Remove [ctree_Forall] and express it using [Forall] and [ctree_flatten]. This
  saves a lot of lines of code.
* Add a [void] value. This value cannot be typed, but will be used as a dummy
  return value for functions with return type [void].

Minor changes:
* Various deciders in preparation of the executable semantics.
* Improve naming and notations.
* Remove obsolete stuff.

* Parametrize refinements with memories. This way, refinements imply typing,
  for example [w1 ⊑{Γ,f@m1↦m2} w2 : τ → (Γ,m1) ⊢ w1 : τ]. This relieves us from
  various hacks.
* Use addresses instead of index/references pairs for lookup and alter
  operations on memories.
* Prove various disjointness properties.