GitLab

All proofs are broken.

- Consistent notation for ↦ of the C language: `x ↦C[lv]{q] v`, which is
  not redefined in every file.
- Many useless stylistic changes.

Now all the small tests work, and the `swap` example passes as well.

The main idea for fixing `vcg_wp` for sequence,
is to change the continuation `(Φ : dval → wp_expr)` of `vcg_wp`
so that it takes `denv` as additional parameter.

Then, in `vcg_wp` all cases, except for the **sequence** and **store** are simply passing the continuation.

The `vcg_wp` for the sequence becomes :

```Coq
| dCSeq de1 de2 => vcg_wp E m de1 R (λ m' _, UMod (vcg_wp E (denv_unlock m') de2 R Φ))
```

The case for  **store** is more subtle.  The critical part is the case
where `vcg_sp E m de1 = Some (mIn, mOut, dv1)` and `dv1 = dLitV (dLitLoc (dLoc i))`,
where the continuation will make use of the function  `denv_replace_full i dv2 m'` whose specification is

```Coq
 Some m' = (denv_replace_full i dv m) →
       ∃ x q dv0 m0,
        (denv_interp E m0 ∗ dloc_interp E (dLoc i) ↦(x   ,  q  ) dval_interp E dv0 ⊣⊢ denv_interp E m) ∧
        (denv_interp E m0 ∗ dloc_interp E (dLoc i) ↦(LLvl, 1%Qp) dval_interp E dv  ⊣⊢ denv_interp E m').
```

In that case, we do not need to generate `IsLoc dv1 ...`, inlining instead the precise form of
`dv1` in the resulting formula, using `denv_replace_full` in the end:

```Coq
| dCStore de1 de2 =>
      match vcg_sp E m de1 with
      | Some (mIn, mOut, dv1) =>
        match dv1 with
        | dLitV (dLitLoc (dLoc i)) =>
          mapsto_star_list m
            (mapsto_wand_list mIn
               (vcg_wp E mIn de2 R (λ m' dv2,
                  mapsto_wand_list mOut
                    (MapstoStarFull (dLoc i) (λ _, (MapstoWand (dLoc i) dv2 LLvl 1%Qp
                         (match (denv_replace_full i dv2 m') with
                          | Some mf => (Φ mf dv2)
                          | None => Base False (*TODO: maybe this is too strong, return just (Φ m' dv2) *)
                          end)))))))
```

Note the comment for the case where `denv_replace_full i dv2 =  None`.
Note also, that for the other cases, including `match vcg_sp E m de2 = Some (mIn, mOut, dv1)`,
the continuation is passed as such, without replacing its content.
For the latter case ( `match vcg_sp E m de2 = Some (mIn, mOut, dv1)`) we probably also need to
update the continuation as described above.

Finally, the correctness statement for the `vcg_wp` becomes :

```Coq
Lemma vcg_wp_correct R E m de Φ :
    wp_interp E (vcg_wp E m de R Φ) ⊢
        awp (dcexpr_interp E de) R
      (λ v, ∃ dv m', ⌜dval_interp E dv = v⌝ ∧ wp_interp E (Φ m' dv)).
 ```

This statement is proven for all cases. Somehow surprisingly, the specification
for `denv_replace_full` was not needed. The reason for that is probably that the correctness
statement only affirms the bare existence of 'm'.

Fix the case of the wp formula for load, by changing the representation of wp_expr (adding MapstoStarFull constructor).

work in progress on adding wp for sequence and alloc. The sequence actually results in some issues with management of the environement

- Use the level resource algebra/lattice.
  This allows us to unlock partially owned locations
- Upclose the mapsto predicates.
  This allows us to "downgrade" unlocked locations.

corretness for vcg_wp and optimize. Some admits remain in relation with level management. The issue with the fractions has to be resolved (see definition of optimize)

rename inhale/exhale -> MapstoStar/MapstoWand (and corresponding functions). Add definition of vcg_wp for Store,Load,BinOp and Ret.

wip on combine function (need for vcg_sp) : need to check the new definition of vcg_sp and reprove the correctness of vcg_wp; NB: combine_function is implemented in an inefficient way (should be reimplemented using sorting functions on lists)