From a0293ba5dcf721366a6444efb4bd17a633491bae Mon Sep 17 00:00:00 2001
From: Ilia Zaichuk <zoickx@ztld.org>
Date: Tue, 13 Aug 2024 17:46:14 +0300
Subject: [PATCH] Prove sizeof/offsetof_struct positivity

---
 coq/Proofs/Revocation.v | 143 +++++++++++++++++++---------------------
 1 file changed, 68 insertions(+), 75 deletions(-)

diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
index 8e77d0326..293d631bb 100644
--- a/coq/Proofs/Revocation.v
+++ b/coq/Proofs/Revocation.v
@@ -5259,10 +5259,7 @@ Module CheriMemoryImplWithProofs
             revert t0 Heqt1.
             induction l;intros.
             ++
-              cbn in H0.
-              inl_inr_inv.
-              setoid_rewrite list.nil_length in H.
-              lia.
+              invc H.
             ++
               cbn in *.
               clear H.
@@ -5295,7 +5292,6 @@ Module CheriMemoryImplWithProofs
               generalize dependent al.
               induction l; intros; cbn in H2.
               **
-                apply ret_inr in H2.
                 now invc H2.
               **
                 apply bind_serr_inv in H2.
@@ -5307,83 +5303,80 @@ Module CheriMemoryImplWithProofs
     -
       clear offsetof_struct_max_offset_pos.
       intros fuel t s l max_offset OF.
-      induction fuel; intros.
-      +
-        simpl in OF.
-        discriminate OF.
-      +
-        cbn in OF.
+      destruct fuel; [ invc OF |].
+      cbn in OF.
 
-        break_match_hyp;[|discriminate OF].
-        break_match_hyp;[| discriminate OF].
-        *
-          (* struct *)
-          apply bind_sassert_inv in OF.
-          destruct OF as [L OF].
-          destruct (Datatypes.length l0) eqn:L0.
-          inv L.
-          clear L.
-
-          apply bind_serr_inv in OF.
-          destruct OF as [x [H1 H2]].
-          break_let.
-          inl_inr_inv.
-          subst.
-
-          remember (match o with
-                    | Some (CoqCtype.FlexibleArrayMember attrs ident qs ty) => l0 ++ [(ident, (attrs, None, qs, ty))]
-                    | None => l0
-                    end) as l0'.
-
-          assert(0 < length l0')%nat.
-          {
-            destruct o.
-            -
-              destruct f.
-              subst l0'.
-              pose proof (app_length l0 [(i, (a, None, q, c))]).
-              rewrite H.
-              lia.
-            -
-              subst.
-              lia.
-          }
-          clear Heql0' l0 L0 Heqo.
-          rename l0' into l0.
+      break_match_hyp;[|discriminate OF].
+      break_match_hyp;[|discriminate OF].
 
-          revert H.
-          induction l0;intros.
-          --
-            setoid_rewrite list.nil_length in H.
-            lia.
-          --
-            cbn in H1.
+      (* struct *)
+      apply bind_sassert_inv in OF.
+      destruct OF as [L OF].
+      destruct (Datatypes.length l0) eqn:L0; invc L.
 
-            apply bind_serr_inv in H1.
-            destruct H1 as [a' [H2 H3]].
-            repeat break_let.
+      apply bind_serr_inv in OF.
+      destruct OF as [x [H1 H2]].
+      break_let.
+      inl_inr_inv.
+      subst.
 
-            destruct a'.
-            rename n0 into max_offset'.
+      remember (match o with
+                | Some (CoqCtype.FlexibleArrayMember attrs ident qs ty) =>
+                    l0 ++ [(ident, (attrs, None, qs, ty))]
+                | None => l0
+                end) as l'.
+      assert (exists x l, l' = x::l).
+      {
+        repeat break_match.
+        all: subst.
+        all: destruct l0; [invc L0 |].
+        all: repeat eexists.
+      }
+      clear Heql'.
+      destruct H as (x & l & L').
+      subst l'.
 
-            apply bind_serr_inv in H2.
-            destruct H2 as [size [H2 H4]].
+      match goal with
+      | [_ : context[monadic_fold_left ?f'] |- _] => remember f' as f
+      end.
+      assert (f_mon : forall x x' off off' a,
+                 f (x, off) a = inr (x', off') ->
+                 (off < off')%nat).
+      {
+        clear - Heqf sizeof_pos.
+        subst.
+        intros.
+        repeat break_let.
+        apply bind_serr_inv in H.
+        do 2 destruct H.
+        cbv [bind] in H0; cbn in H0.
+        break_match; try discriminate.
+        apply ret_inr in H0.
+        invc H0.
+        apply  sizeof_pos in H.
+        lia.
+      }
+      clear - f_mon H1; rename H1 into F.
 
-            apply bind_serr_inv in H4.
-            destruct H4 as [align [H4 H5]].
-            inl_inr_inv.
+      cbn in F.
+      apply bind_serr_inv in F.
+      destruct F as ((x0, off0) & F0 & F).
+      apply f_mon in F0.
 
-            assert(0<max_offset')%nat.
-            {
-              cut (0<size)%nat.
-              intros H0.
-              lia.
-              clear - sizeof_pos H2.
-              eapply sizeof_pos.
-              eauto.
-            }
-            admit.
-  Admitted.
+      generalize dependent x0.
+      generalize dependent off0.
+      induction l; intros.
+      +
+        now invc F.
+      +
+        cbn in F.
+        apply bind_serr_inv in F.
+        destruct F as ((x1 & off1) & F1 & F).
+        apply IHl in F.
+        easy.
+        apply f_mon in F1.
+        lia.
+  Qed.
 
   Fact amap_add_list_not_at
     {T: Type}