Get rid of some level-related admits in vcgen

theories/vcgen/denv.v

@@ -179,7 +179,7 @@ Section denv_spec.
      iIntros (k y ?) "H". simplify_eq/=. destruct y as [di|]; last first.
      - simpl. by iModIntro.
      - destruct di as [x q dv]. simpl.
-       destruct x; iModIntro. (* TODO DF: this is completely fubard *)
-   Admitted.
+       destruct x; iModIntro; iFrame.
+   Qed.
 
 End denv_spec.

theories/vcgen/vcgen.v

@@ -368,7 +368,7 @@ Section vcg_spec.
                   denv_interp E mIn ∗
                   wp_interp E (mapsto_wand_list (denv_merge mIn mOut)
                    (MapstoStar dl 1 (λ _ : dval, MapstoWand dl dv LLvl 1 (Φ dv)))))%I
-         with "[Hde1 HmIn] [$Hde2]").
+         with "[Hde1 HmIn] Hde2").
         * iApply (awp_wand with "Hde1").
           iIntros (v) "H".
           iDestruct "H" as (dv1 <-) "Hwp". simplify_eq /=.
@@ -473,7 +473,9 @@ Section vcg_spec.
             rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
           rewrite -(denv_delete_full_interp _ i m); last eassumption.
           rewrite IHΦ. iIntros "Hdv".
-          iIntros "[Hm' Hi]". iFrame. admit. (* TODO DF: take a look at this *)
+          iIntros "[Hm' Hi]". iFrame.
+          iSplitL "Hi"; last by iApply "Hdv".
+          by iApply mapsto_downgrade.
         * (* q <> 1 *)
           remember (denv_delete_frac i m) as Hdl.
           destruct Hdl as [[[m' q'] dv']|]; last first.
@@ -487,7 +489,9 @@ Section vcg_spec.
             rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv". }
           rewrite IHΦ. iIntros "Hdv'".
           rewrite -(denv_delete_frac_interp _ i m); last eassumption.
-          iIntros "[Hm Hl]". iFrame. admit. (* TODO DF: issue with levels *)
+          iIntros "[Hm Hi]". iFrame.
+          iSplitL "Hi"; last by iApply "Hdv'".
+          by iApply mapsto_downgrade.
       + (* location wasn't found *)
         simpl. iIntros "[Hl Hdv]".
         rewrite IHΦ. iIntros "Hm". iFrame. by iApply "Hdv".
@@ -511,7 +515,7 @@ Section vcg_spec.
     - iIntros "HΦ Hm".
       rewrite IHΦ. iDestruct (denv_unlock_interp with "Hm") as "Hm".
       iModIntro. by iApply "HΦ".
-  Admitted.
+  Qed.
 
   Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
     MapstoListFromEnv Γs_in Γs_out Γls →