Finished proof automation of PredicateRequest for struct with folding (using hints). (#58)

vzaliva · olympichek · cp526 · web-flow · commit 9027174addc2 · 2025-04-24T10:15:54.000+01:00
* Simplify folding hints * Implement struct folding automation * Ensure use of the right context in hints simplification * bump up Coq version. fixes #63 --------- Co-authored-by: Valerii Huhnin <33845529+olympichek@users.noreply.github.com> Co-authored-by: Christopher Pulte <cp526@cam.ac.uk>
diff --git a/coq/Cn/BaseTypes.v b/coq/Cn/BaseTypes.v
@@ -152,7 +152,7 @@ Lemma option_eq_dec {A : Type}
       forall (o1 o2 : option A), {o1 = o2} + {o1 <> o2}.
 Proof.
   decide equality.
-Qed.
+Defined.
 
 Module BasetTypes_t_as_MiniDecidableType <: MiniDecidableType.
   Definition t := t.
diff --git a/coq/Reasoning/ProofAutomation.v b/coq/Reasoning/ProofAutomation.v
@@ -93,7 +93,7 @@ Qed.
 
 
 (* [struct_resource_inference_step] constructor pre-condition proof *)
- Ltac2 prove_struct_resource_inference_step () :=
+ Ltac2 prove_struct_resource_inference_step (log_entry:constr) :=
  match! goal with
  | [ |- exists field_res,
         unfold_all _ _ field_res /\
@@ -113,7 +113,12 @@ Qed.
      Std.split false NoBindings;
      Control.focus 1 1 (fun () =>
       (* Proof using computational reflection: *)
-      Control.shelve ()
+      ltac1:(apply unfold_all_singleton_eq);
+      ltac1:(log_entry |- apply unfold_all_explicit_eq with (unfold_changed := (get_hints_from_log_entry log_entry))) 
+        (Ltac1.of_constr log_entry);
+      ltac1:(apply unfold_all_explicit_fun_eq);
+      ltac1:(vm_compute);
+      ltac1:(reflexivity)
      );  (* unfold predicate *)
      Control.focus 1 1 (fun () =>
       pairwise_decidability (constr:(Resource_as_MiniDecidableType.eq_dec)) in_res_list ;
@@ -160,34 +165,38 @@ Ltac2 prove_unfold_step (hints:constr) :=
         Predicate.pointer := _; Predicate.iargs := _ 
       |}
       _ ?hints _) ] =>
-       verbose_msg (smsg "Checking PredicateRequest for Struct");
-       verbose_print_constr "    Situation: " s;
-       verbose_print_constr "    Predicate symbol name: " isym;
-       let lhints := destruct_list (constr:(log_entry)) hints in
-       verbose_msg (Message.concat (Message.of_string "    Number of hints: ") (Message.of_int (List.length lhints)));
-       Std.constructor_n false 3 NoBindings; (* apply struct_resource_inference_step *)
-       Control.focus 1 1 (fun () => Std.reflexivity ());
-       Control.focus 1 1 (fun () => Std.reflexivity ());
-       Control.focus 1 1 (fun () => Std.reflexivity ());
-       Control.focus 1 1 (fun () => Std.reflexivity ());
-       Control.focus 1 1 (fun () => Std.reflexivity ());
-       Control.focus 1 1 (fun () => Std.reflexivity ());
-       Control.focus 1 1 (fun () => Std.reflexivity ());
-       Control.focus 1 1 (fun () => 
-        let clause := { on_hyps := None; on_concl := AllOccurrences } in
-          Std.unfold [(const_to_const_reference constr:(@ctx_resources_set), AllOccurrences)] clause;
-          Std.cbn 
-          { rStrength := Std.Norm;
-            rBeta := true;
-            rMatch := true;
-            rFix := true;
-            rCofix := true;
-            rZeta := true;
-            rDelta := true;
-            rConst := [const_to_const_reference constr:(@set_from_list); const_to_const_reference constr:(@Sym.map_from_list)]
-          } clause ;
-          prove_struct_resource_inference_step ()
-       )
+        match! goal with
+        | [ |- log_entry_valid ?log_entry ] =>
+          verbose_msg (smsg "Checking PredicateRequest for Struct");
+          verbose_print_constr "    Situation: " s;
+          verbose_print_constr "    Predicate symbol name: " isym;
+          let lhints := destruct_list (constr:(log_entry)) hints in
+          verbose_msg (Message.concat (Message.of_string "    Number of hints: ") (Message.of_int (List.length lhints)));
+          Std.constructor_n false 3 NoBindings; (* apply struct_resource_inference_step *)
+          Control.focus 1 1 (fun () => Std.reflexivity ());
+          Control.focus 1 1 (fun () => Std.reflexivity ());
+          Control.focus 1 1 (fun () => Std.reflexivity ());
+          Control.focus 1 1 (fun () => Std.reflexivity ());
+          Control.focus 1 1 (fun () => Std.reflexivity ());
+          Control.focus 1 1 (fun () => Std.reflexivity ());
+          Control.focus 1 1 (fun () => Std.reflexivity ());
+          Control.focus 1 1 (fun () => 
+            let clause := { on_hyps := None; on_concl := AllOccurrences } in
+              Std.unfold [(const_to_const_reference constr:(@ctx_resources_set), AllOccurrences)] clause;
+              Std.cbn 
+              { rStrength := Std.Norm;
+                rBeta := true;
+                rMatch := true;
+                rFix := true;
+                rCofix := true;
+                rZeta := true;
+                rDelta := true;
+                rConst := [const_to_const_reference constr:(@set_from_list); const_to_const_reference constr:(@Sym.map_from_list)]
+              } clause ;
+              prove_struct_resource_inference_step log_entry
+          )
+        end
+        
     (* PredicateRequest for non-Struct *)
   | [ |- log_entry_valid (PredicateRequest _ ?s ?p _ _ _)] =>
        (* PredicateRequest case *)
diff --git a/coq/Reasoning/ResourceInference.v b/coq/Reasoning/ResourceInference.v
@@ -15,10 +15,13 @@ Import ListNotations.
 Inductive provable (g:Global.t): LCSet.t -> LogicalConstraints.t -> Prop :=
 | solvable_SMT: forall lc it, provable g lc it.
 
+(* Helper function to get a list of resources from the contex *)
+Definition ctx_resources_list (l: (list (Resource.t * Z)) * Z) : list Resource.t :=
+  List.map fst (fst l).
+
 (* Helper function to get a set of resources from the contex *)
-Definition ctx_resources_set (l:((list (Resource.t * Z)) * Z)) : ResSet.t
-  :=
-  Resource.set_from_list (List.map fst (fst l)).
+Definition ctx_resources_set (l: (list (Resource.t * Z)) * Z) : ResSet.t :=
+  Resource.set_from_list (ctx_resources_list l).
 
 Inductive term_is_struct: Terms.term BaseTypes.t -> Prop :=
 | term_is_struct_intro: forall tag fields,
@@ -521,6 +524,34 @@ Inductive unfold_one (globals:Global.t): Resource.t -> ResSet.t -> Prop :=
          iout)
       out_res.
 
+Definition apply_for_subsumed (iinit: init) (f : init -> bool) : bool :=
+  match iinit with
+  | Init => f Init
+  | Uninit => f Uninit || f Init
+  end.
+
+Lemma apply_for_subsumed_spec:
+  forall iinit f t, apply_for_subsumed iinit f = true ->
+  exists iinit', subsumed (Owned t iinit) (Owned t iinit') /\ f iinit' = true.
+Proof.
+  intros iinit f t H.
+  unfold apply_for_subsumed in H.
+  destruct iinit.
+  - exists Init; split.
+    + apply Subsumed_equal.
+      reflexivity.
+    + apply H.
+  - apply orb_true_iff in H as [H | H].
+    + exists Uninit; split.
+      * apply Subsumed_equal.
+        reflexivity.
+      * apply H.
+    + exists Init; split.
+      * apply Subsumed_owned.
+        reflexivity.
+      * apply H.
+Qed.
+
 (* Computable version of unfold_one predicate *) 
 Definition unfold_one_fun (globals:Global.t) (r : Resource.t) (out_res: list Resource.t) : bool :=
   match r with
@@ -532,9 +563,10 @@ Definition unfold_one_fun (globals:Global.t) (r : Resource.t) (out_res: list Res
         match SymMap.find isym globals.(Global.struct_decls) with
         | Some sdecl =>
           (List.length sdecl =? List.length out_res) &&
-          List.forallb
-            (fun '(piece, r) => struct_piece_to_resource_fun piece iinit ipointer iargs isym iout r)
-            (List.combine sdecl out_res)
+          apply_for_subsumed iinit (fun iinit' =>
+            List.forallb
+              (fun '(piece, r) => struct_piece_to_resource_fun piece iinit' ipointer iargs isym iout r)
+              (List.combine sdecl out_res))
         | None => false
         end
   | _ => false
@@ -559,9 +591,10 @@ Proof.
   apply SymMap.find_2 in Hf.
   assert (piece_def : Memory.struct_piece) by (repeat constructor).
   assert (res_def : Resource.t) by (repeat constructor).
-  eapply unfold_one_struct with (iinit' := i).
-  { apply Subsumed_equal.
-    reflexivity. }
+  apply apply_for_subsumed_spec with (t := Struct s) in H.
+  destruct H as [i' [Hi H]]. 
+  eapply unfold_one_struct with (iinit' := i').
+  { apply Hi. }
   { apply Hf. }
   intros r; split.
   - intros Hr.
@@ -616,6 +649,87 @@ Inductive unfold_all (globals:Global.t): ResSet.t -> ResSet.t -> Prop :=
     ResSet.Equal input output ->
     unfold_all globals input output.
 
+Lemma unfold_one_Proper : Proper (eq ==> eq ==> ResSet.Equal ==> iff) unfold_one.
+Proof.
+  intros globals globals' Hglobals r r' Hr rs rs' Hrs.
+  subst r' globals'.
+  enough (forall r rs rs', ResSet.Equal rs rs' -> unfold_one globals r rs -> unfold_one globals r rs') as H.
+  { split; intros H1.
+    - eapply H.
+      + apply Hrs.
+      + apply H1.
+    - eapply H.
+      + symmetry; apply Hrs.
+      + apply H1. }
+  clear.
+  intros r rs rs' Hrs H.
+  inversion H; subst; clear H.
+  econstructor; eauto.
+  intros r; split; intros Hr.
+  - apply H2.
+    eapply ResSetDecide.F.In_m.
+    + reflexivity.
+    + apply Hrs.
+    + apply Hr.
+  - eapply ResSetDecide.F.In_m.
+    + reflexivity.
+    + symmetry.
+      apply Hrs.
+    + apply H2, Hr.
+Qed.
+
+Lemma unfold_all_Proper : Proper (eq ==> ResSet.Equal ==> ResSet.Equal ==> iff) unfold_all.
+Proof.
+  intros globals globals' Hglobals r1 r1' Hr1 r2 r2' Hr2.
+  subst globals'.
+  enough (forall r1 r1' r2 r2', ResSet.Equal r1 r1' -> ResSet.Equal r2 r2' ->
+          unfold_all globals r1 r2 -> unfold_all globals r1' r2') as H.
+  { split; intros H1.
+    - eapply H.
+      + apply Hr1.
+      + apply Hr2.
+      + apply H1.
+    - eapply H.
+      + symmetry; apply Hr1.
+      + symmetry; apply Hr2.
+      + apply H1. }
+  clear.
+  intros r1 r1' r2 r2' Hr1 Hr2 H.
+  revert r1' r2' Hr1 Hr2.
+  induction H; intros r1' r2' Hr1 Hr2.
+  - eapply unfold_all_step with (input' := input').
+    + apply Hr1, H.
+    + apply H0.
+    + ResSetDecide.fsetdec.
+    + apply IHunfold_all.
+      * reflexivity.
+      * apply Hr2.
+  - apply unfold_all_fixpoint.
+    + intros H1.
+      apply H.
+      destruct H1 as [r [Hr H1]].
+      exists r; split; try assumption.
+      apply Hr1, Hr.
+    + transitivity input.
+      { apply Equivalence_Symmetric, Hr1. }
+      transitivity output.
+      { apply H0. }
+      apply Hr2.
+Qed. 
+
+Lemma unfold_all_singleton_eq:
+  forall globals r output,
+  unfold_all globals (Resource.set_from_list [r]) output <->
+  unfold_all globals (ResSet.singleton r) output.
+Proof.
+  intros globals r output.
+  eapply unfold_all_Proper.
+  - reflexivity.
+  - cbn.
+    ResSetDecide.fsetdec.
+  - reflexivity.
+Qed.
+
 (* A version of `unfold_all`, using hints *)
 Inductive unfold_all_explicit (globals:Global.t):
   list (Resource.t * unpack_result) -> ResSet.t -> ResSet.t -> Prop :=
@@ -746,6 +860,40 @@ Qed.
 Definition unfold_step_flatten (l : list unfold_step): unfold_changed :=
   List.concat (List.map fst l).
 
+Definition get_resources_from_log (log_entries : log) : list Resource.t :=
+  List.fold_right (fun log_entry rs =>
+    match log_entry with
+    | PredicateRequest _ _ _ (p, o) _ _ => (Request.P p, o) :: rs
+    | UnfoldResources _ _ _ _ => rs (* probably shouldn't happen *)
+    end) [] log_entries.
+
+Definition resource_set_init (r : Resource.t) : Resource.t :=
+  match r with
+  | (Request.P {| Predicate.name := Request.Owned t _;
+                  Predicate.pointer := p;
+                  Predicate.iargs := args |}, out) =>
+    (Request.P {| Predicate.name := Request.Owned t Init;
+                  Predicate.pointer := p;
+                  Predicate.iargs := args |}, out)
+  | r => r
+  end.
+
+Definition resource_set_correct_init_status (c : Context.t) (r : Resource.t) : Resource.t := 
+  if List.existsb (fun r' => bool_of_sum (Resource_as_DecidableType.eq_dec r r')) (ctx_resources_list c.(resources))
+  then r
+  else resource_set_init r.
+
+Fixpoint get_hints_from_log_entry (log_entry : log_entry) : unfold_changed :=
+  match log_entry with
+  | PredicateRequest _ _ _ _ [] _ => []
+  | PredicateRequest ic _ _ (p, o) log_entries _ =>
+      let r := (Request.P p, o) in
+      let unfolded_r := List.map (resource_set_correct_init_status ic) (get_resources_from_log log_entries) in
+      let hints_inner := List.concat (List.map get_hints_from_log_entry log_entries) in
+      (r, UnpackRES unfolded_r) :: hints_inner
+  | UnfoldResources _ _ _ _ => [] (* probably shouldn't happen *)
+  end.
+
 (** Inductive predicate which defines correctness of resource unfolding step *)
 Inductive unfold_step : Context.t -> Context.t -> Prop :=
 | simple_unfold_step:
diff --git a/lib/resourceInference.ml b/lib/resourceInference.ml
@@ -399,7 +399,7 @@ module General = struct
       | _ ->
         let@ ftyp, rw_time, l' =
           parametric_ftyp_args_request_step
-            resource_request
+            (resource_request ~simplify_prooflog:true)
             IT.subst
             loc
             uiinfo
@@ -412,24 +412,35 @@ module General = struct
     loop ftyp [] []
 
 
-  and resource_request loc uiinfo (request : Req.t)
+  and resource_request ?(simplify_prooflog = false) loc uiinfo (request : Req.t)
     : (Resource.t * int list * Prooflog.log) option m
     =
     match request with
     | P request ->
       let@ c = get_typing_context () in
       let@ result = predicate_request loc uiinfo request in
       let@ c' = get_typing_context () in
+      let@ simp_ctxt = simp_ctxt () in
       return
         (Option.map
-           (fun ((p, o), changed_or_deleted, l) ->
+           (fun ((p, Resource.O o), changed_or_deleted, l) ->
               let hints =
-                if Prooflog.is_enabled () then
-                  [ Prooflog.PredicateRequest (c, fst uiinfo, request, (p, o), l, c') ]
+                if Prooflog.is_enabled () then (
+                  let p, o =
+                    if not simplify_prooflog then
+                      (p, o)
+                    else (
+                      let p = Simplify.Request.Predicate.simp simp_ctxt p in
+                      let o = Simplify.IndexTerms.simp simp_ctxt o in
+                      (p, o))
+                  in
+                  [ Prooflog.PredicateRequest
+                      (c, fst uiinfo, request, (p, Resource.O o), l, c')
+                  ])
                 else
                   []
               in
-              ((Req.P p, o), changed_or_deleted, hints))
+              ((Req.P p, Resource.O o), changed_or_deleted, hints))
            result)
     | Q request ->
       let@ result = qpredicate_request loc uiinfo request in
@@ -447,7 +458,7 @@ module General = struct
   let ftyp_args_request_step rt_subst loc situation original_resources ftyp =
     let@ rt, _rw_time, l =
       parametric_ftyp_args_request_step
-        resource_request
+        (resource_request ~simplify_prooflog:false)
         rt_subst
         loc
         situation
