From cddec4a65582875a4ae3a5c0081ce1b04d9b3f1d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <Lennard.Gaeher@ibm.com>
Date: Thu, 21 Dec 2023 12:41:25 +0100
Subject: [PATCH] improve script

---
 scripts/install-typesystem.sh   | 3 +++
 theories/rust_typing/programs.v | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/scripts/install-typesystem.sh b/scripts/install-typesystem.sh
index 3907af2f..5f0c477b 100755
--- a/scripts/install-typesystem.sh
+++ b/scripts/install-typesystem.sh
@@ -5,5 +5,8 @@
 # - REFINEDRUST_ROOT: the root directory of the RefinedRust checkout
 
 opam pin remove refinedrust
+opam pin remove coq-lithium
+opam remove coq-lithium
+opam remove refinedrust
 opam pin add coq-lithium.dev $REFINEDRUST_ROOT -y
 opam pin add refinedrust.dev $REFINEDRUST_ROOT -y
diff --git a/theories/rust_typing/programs.v b/theories/rust_typing/programs.v
index b9a68efe..75357751 100644
--- a/theories/rust_typing/programs.v
+++ b/theories/rust_typing/programs.v
@@ -534,12 +534,12 @@ Section judgments.
 
   Global Program Instance learn_hyp_loc_in_bounds l off1 off2 :
     LearnFromHyp (loc_in_bounds l off1 off2)%I | 10 :=
-    {| learn_from_hyp_Q := ⌜(0 < l.2 - off1)%Z ∧ (l.2 + off2 ≤ MaxInt usize_t)%Z⌝ |}.
+    {| learn_from_hyp_Q := ⌜enter_cache_hint (0 < l.2 - off1)%Z⌝ ∗ ⌜enter_cache_hint (l.2 + off2 ≤ MaxInt usize_t)%Z⌝ |}.
   Next Obligation.
     iIntros (l off1 off2 ? ?) "Hlb".
     iPoseProof (loc_in_bounds_ptr_in_range with "Hlb") as "%Hinrange".
     iFrame. iModIntro. iPureIntro.
-    move: Hinrange. rewrite /min_alloc_start.
+    move: Hinrange. rewrite /min_alloc_start /enter_cache_hint.
     split; first lia.
     rewrite MaxInt_eq.
     specialize (max_alloc_end_le_usize). lia.
-- 
GitLab