Dummy module for module merge/split

[alxest]

Use case

In module merge, we prove sth like this: ctx [ModTuple mdl mdr] >= ctx[mdl ++ mdr] Here, source's Midx.ts are ctx ++ mdl while target's are ctx ++ mdl ++ mdr. Therefore, source can have less undefined behavior in linking. To solve this nicely, we can put dummy module that only has Midx.t but nothing else. Then, we can prove something like this: ctx [ModTuple mdl mdr ++ dummy mdr] >= ctx[mdl ++ mdr].

Problem

In order to define such dummy module, we should have identity element of Sk.t. (i.e. we need sth like this: forall sk, link sk Sk.empty = Some sk) However, CompCert's PTree does not support intentional equality, so we can't get such identity element.

Solution

1) Extend PTree theorems. 2) Use some equivalence class rather than leibniz equality --> it is an expensive solution... 3) Do not link Sk.t, instead link prog_defmap Sk.t whose identity element is easily PTree.empty 4) Put dummy_midxs: list Midx.t in Mod.t, just to evoke UB 5) Just quantify mdr.(midx) \notin ctx

[alxest]

Quick test:

  Let x :=
    let t0 := (PTree.set 1%positive 10 (PTree.set 3%positive 30 (PTree.set 2%positive 20 (@PTree.empty _)))) in
    let t1 := PTree.set 2%positive 20 (PTree.set 5%positive 50 (PTree.remove 2%positive t0)) in
    t1
  .
  Let p := Eval compute in x.
  Let q := Eval compute in (PTree_Properties.of_list (PTree.elements x)).
  Print p.
  Print q.
  Goal p = q. refl. Qed.