From ca0e37d1f713dd063babbecf403fa7bd2f3ce16d Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Fri, 25 Oct 2024 10:50:38 -0700
Subject: [PATCH] extra lemmas about SeqMatch, Trade

---
 lib/pulse/lib/Pulse.Lib.SeqMatch.Util.fst     | 256 ++++++++++++++
 lib/pulse/lib/pledge/Pulse.Lib.Trade.Util.fst | 317 ++++++++++++++++++
 2 files changed, 573 insertions(+)
 create mode 100644 lib/pulse/lib/Pulse.Lib.SeqMatch.Util.fst
 create mode 100644 lib/pulse/lib/pledge/Pulse.Lib.Trade.Util.fst

diff --git a/lib/pulse/lib/Pulse.Lib.SeqMatch.Util.fst b/lib/pulse/lib/Pulse.Lib.SeqMatch.Util.fst
new file mode 100644
index 000000000..31804f2c4
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.SeqMatch.Util.fst
@@ -0,0 +1,256 @@
+module Pulse.Lib.SeqMatch.Util
+#lang-pulse
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Trade
+include Pulse.Lib.SeqMatch
+module Trade = Pulse.Lib.Trade.Util
+
+ghost
+fn seq_list_match_nil_elim_trade
+  (#t #t': Type0)
+  (c: Seq.seq t)
+  (v: list t')
+  (item_match: (t -> (v': t' { v' << v }) -> slprop))
+  (p q: slprop)
+requires
+    Trade.trade
+      (seq_list_match c v item_match ** p)
+      q **
+    pure (
+      c `Seq.equal` Seq.empty /\
+      Nil? v
+    )
+ensures
+    Trade.trade p q
+{
+  seq_list_match_nil_intro c v item_match;
+  Trade.elim_hyp_l _ p q
+}
+
+ghost
+fn seq_list_match_nil_intro_trade
+  (#t #t': Type0)
+  (c: Seq.seq t)
+  (v: list t')
+  (item_match: (t -> (v': t' { v' << v }) -> slprop))
+  (p q: slprop)
+requires
+    Trade.trade p q **
+    pure (
+      c `Seq.equal` Seq.empty /\
+      Nil? v
+    )
+ensures
+    Trade.trade (seq_list_match c v item_match ** p) q
+{
+  ghost
+  fn aux (_: unit)
+  requires
+    Trade.trade p q ** (seq_list_match c v item_match ** p)
+  ensures
+    q
+  {
+    seq_list_match_nil_elim c v item_match;
+    Trade.elim _ _;
+  };
+  Trade.intro _ _ _ aux
+}
+
+ghost
+fn seq_list_match_cons_elim_trade
+  (#t #t': Type0)
+  (c: Seq.seq t)
+  (v: list t' { Cons? v \/ Seq.length c > 0 })
+  (item_match: (t -> (v': t' { v' << v }) -> slprop))
+requires
+    (seq_list_match c v item_match)
+returns res: (squash (Cons? v /\ Seq.length c > 0))
+ensures
+    (item_match (Seq.head c) (List.Tot.hd v) **
+      seq_list_match (Seq.tail c) (List.Tot.tl v) item_match **
+      trade
+        (item_match (Seq.head c) (List.Tot.hd v) **
+          seq_list_match (Seq.tail c) (List.Tot.tl v) item_match
+        )
+        (seq_list_match c v item_match)
+    )
+{
+  seq_list_match_cons_elim c v item_match;
+  ghost
+  fn aux ()
+    requires emp **
+      (item_match (Seq.head c) (List.Tot.hd v) **
+          seq_list_match (Seq.tail c) (List.Tot.tl v) item_match
+      )
+    ensures
+      (seq_list_match c v item_match)
+  {
+    Seq.cons_head_tail c;
+    seq_list_match_cons_intro (Seq.head c) (List.Tot.hd v) (Seq.tail c) (List.Tot.tl v) item_match
+  };
+  Trade.intro _ _ _ aux;
+  ()
+}
+
+ghost
+fn seq_list_match_cons_intro_trade
+  (#t #t': Type0)
+  (a: t)
+  (a' : t')
+  (c: Seq.seq t)
+  (v: list t')
+  (item_match: (t -> (v': t' { v' << a' :: v }) -> slprop))
+requires
+    (item_match a a' ** seq_list_match c v item_match)
+ensures
+    (seq_list_match (Seq.cons a c) (a' :: v) item_match **
+      Trade.trade
+        (seq_list_match (Seq.cons a c) (a' :: v) item_match)
+        (item_match a a' ** seq_list_match c v item_match)
+    )
+{
+  seq_list_match_cons_intro a a' c v item_match;
+  ghost fn aux (_: unit)
+  requires
+    emp ** seq_list_match (Seq.cons a c) (a' :: v) item_match
+  ensures
+    item_match a a' ** seq_list_match c v item_match
+  {
+    let _ = seq_list_match_cons_elim (Seq.cons a c) (a' :: v) item_match;
+    rewrite (item_match (Seq.head (Seq.cons a c)) (List.Tot.hd (a' :: v))) as (item_match a a');
+    Seq.lemma_tl a c;
+    rewrite (seq_list_match (Seq.tail (Seq.cons a c)) (List.Tot.tl (a' :: v)) item_match) as (seq_list_match c v item_match)
+  };
+  Trade.intro _ _ _ aux
+}
+
+ghost
+fn seq_list_match_singleton_intro_trade
+  (#t #t': Type0)
+  (a: t)
+  (a': t')
+  (item_match: (t -> (v': t' { v' << [a'] }) -> slprop))
+requires
+  item_match a a'
+ensures
+  seq_list_match (Seq.cons a Seq.empty) [a'] item_match **
+  Trade.trade
+    (seq_list_match (Seq.cons a Seq.empty) [a'] item_match)
+    (item_match a a')
+{
+  seq_list_match_nil_intro Seq.empty [] item_match;
+  seq_list_match_cons_intro_trade a a' Seq.empty [] item_match;
+  ghost fn aux (_: unit)
+  requires
+    Trade.trade
+      (seq_list_match (Seq.cons a Seq.empty) [a'] item_match)
+      (item_match a a' ** seq_list_match Seq.empty [] item_match) **
+    seq_list_match (Seq.cons a Seq.empty) [a'] item_match
+  ensures
+    item_match a a'
+  {
+    Trade.elim _ _;
+    seq_list_match_nil_elim Seq.empty [] item_match
+  };
+  Trade.intro _ _ _ aux
+}
+
+ghost
+fn
+seq_list_match_append_intro_trade
+  (#t #t': Type0) // FIXME: universe polymorphism
+  (item_match: (t -> t' -> slprop))
+  (c1: Seq.seq t)
+  (l1: list t')
+  (c2: Seq.seq t)
+  (l2: list t')
+requires
+    (seq_list_match c1 l1 item_match ** seq_list_match c2 l2 item_match)
+ensures
+    seq_list_match (c1 `Seq.append` c2) (l1 `List.Tot.append` l2) item_match **
+    Trade.trade
+      (seq_list_match (c1 `Seq.append` c2) (l1 `List.Tot.append` l2) item_match)
+      (seq_list_match c1 l1 item_match ** seq_list_match c2 l2 item_match)
+{
+  seq_list_match_length item_match c1 l1;
+  seq_list_match_append_intro item_match c1 l1 c2 l2;
+  ghost fn aux (_: unit)
+  requires
+    emp ** seq_list_match (c1 `Seq.append` c2) (l1 `List.Tot.append` l2) item_match
+  ensures
+    seq_list_match c1 l1 item_match ** seq_list_match c2 l2 item_match
+  {
+    seq_list_match_append_elim item_match c1 l1 c2 l2
+  };
+  Trade.intro _ _ _ aux
+}
+
+ghost
+fn seq_list_match_append_elim_trade
+  (#t #t': Type0) // FIXME: universe polymorphism
+  (item_match: (t -> t' -> slprop))
+  (c1: Seq.seq t)
+  (l1: list t')
+  (c2: Seq.seq t)
+  (l2: list t')
+requires
+    (seq_list_match (c1 `Seq.append` c2) (l1 `List.Tot.append` l2) item_match **
+    pure (Seq.length c1 == List.Tot.length l1 \/
+      Seq.length c2 == List.Tot.length l2))
+ensures
+    seq_list_match c1 l1 item_match ** seq_list_match c2 l2 item_match **
+    Trade.trade
+      (seq_list_match c1 l1 item_match ** seq_list_match c2 l2 item_match)
+      (seq_list_match (c1 `Seq.append` c2) (l1 `List.Tot.append` l2) item_match) **
+    pure (
+      Seq.length c1 == List.Tot.length l1 /\
+      Seq.length c2 == List.Tot.length l2
+    )
+{
+  seq_list_match_append_elim item_match c1 l1 c2 l2;
+  ghost fn aux (_: unit)
+  requires
+    emp ** (seq_list_match c1 l1 item_match ** seq_list_match c2 l2 item_match)
+  ensures
+    seq_list_match (c1 `Seq.append` c2) (l1 `List.Tot.append` l2) item_match
+  {
+    seq_list_match_append_intro item_match c1 l1 c2 l2
+  };
+  Trade.intro _ _ _ aux
+}
+
+open Pulse.Lib.Stick
+
+ghost
+fn seq_list_match_index_trade
+  (#t1 #t2: Type0)
+  (p: t1 -> t2 -> slprop)
+  (s1: Seq.seq t1)
+  (s2: list t2)
+  (i: nat)
+requires
+    (seq_list_match s1 s2 p ** pure (
+      (i < Seq.length s1 \/ i < List.Tot.length s2)
+    ))
+returns res: (squash (i < Seq.length s1 /\ List.Tot.length s2 == Seq.length s1))
+ensures
+    (
+      p (Seq.index s1 i) (List.Tot.index s2 i) **
+      (p (Seq.index s1 i) (List.Tot.index s2 i) `Trade.trade`
+        seq_list_match s1 s2 p)
+    )
+{
+  seq_list_match_index p s1 s2 i;
+  ghost fn aux (_: unit)
+  requires
+    (p (Seq.index s1 i) (List.Tot.index s2 i) @==>
+      (seq_list_match s1 s2 p)) **
+    p (Seq.index s1 i) (List.Tot.index s2 i)
+  ensures
+    seq_list_match s1 s2 p
+  {
+    Pulse.Lib.Stick.elim_stick (p (Seq.index s1 i) (List.Tot.index s2 i)) (seq_list_match s1 s2 p);
+  };
+  Trade.intro _ _ _ aux;
+  ()
+}
diff --git a/lib/pulse/lib/pledge/Pulse.Lib.Trade.Util.fst b/lib/pulse/lib/pledge/Pulse.Lib.Trade.Util.fst
new file mode 100644
index 000000000..e751a26a2
--- /dev/null
+++ b/lib/pulse/lib/pledge/Pulse.Lib.Trade.Util.fst
@@ -0,0 +1,317 @@
+module Pulse.Lib.Trade.Util
+#lang-pulse
+open Pulse.Lib.Pervasives
+include Pulse.Lib.Trade
+
+module T = FStar.Tactics
+
+let intro
+  (#[T.exact (`emp_inames)] is:inames)
+= intro_trade #is
+
+let elim
+  (#is:inames)
+= elim_trade #is
+
+ghost
+fn refl_explicit
+//  (#[T.exact (`emp_inames)] is:inames) // FIXME: Pulse shouldn't remove this implicit marker
+  (is: inames)
+  (p: slprop)
+requires emp
+ensures (trade #is p p)
+{
+  ghost fn aux (_: unit)
+    requires emp ** p
+    ensures p
+    opens is
+  {
+    ()
+  };
+  intro_trade p p emp aux
+}
+
+let refl 
+  (#[T.exact (`emp_inames)] is:inames)
+= refl_explicit is
+
+ghost
+fn refl'_explicit
+//  (#[T.exact (`emp_inames)] is:inames) // FIXME: Pulse shouldn't remove this implicit marker
+  (is:inames)
+  (p q: slprop)
+requires pure (p == q)
+ensures (trade #is p q)
+{
+  refl #is p;
+  rewrite (trade #is p p) as (trade #is p q)
+}
+
+let refl'
+  (#[T.exact (`emp_inames)] is:inames)
+= refl'_explicit is
+
+ghost
+fn curry
+  (#is: inames)
+  (p q r:slprop)
+   requires trade #is (p ** q) r
+   ensures trade #emp_inames p (trade #is q r)
+{
+    ghost fn aux (_:unit)
+    requires (trade #is (p ** q) r) ** p
+    ensures trade #is q r
+    { 
+        ghost fn aux (_:unit)
+        requires ((trade #is (p ** q) r) ** p) ** q
+        ensures r
+        opens is
+        { 
+            elim _ _;
+        };
+        intro _ _ _ aux;
+    };
+    intro _ _ _ aux;
+}
+
+let trans
+  (#is : inames)
+= trade_compose #is
+
+ghost
+fn comm_l (#is: inames) (p q r:slprop)
+   requires trade #is (p ** q) r
+   ensures trade #is (q ** p) r
+{
+  slprop_equivs ();
+  rewrite (trade #is (p ** q) r) as (trade #is (q ** p) r)
+}
+
+ghost
+fn comm_r (#is: inames) (p q r:slprop)
+   requires trade #is p (q ** r)
+   ensures trade #is p (r ** q)
+{
+  slprop_equivs ();
+  rewrite (trade #is p (q ** r)) as (trade #is p (r ** q))
+}
+
+ghost
+fn assoc_hyp_l (#is: inames) (p q r s:slprop)
+   requires trade #is (p ** (q ** r)) s
+   ensures trade #is ((p ** q) ** r) s
+{
+  slprop_equivs ();
+  rewrite (trade #is (p ** (q ** r)) s) as (trade #is ((p ** q) ** r) s)
+}
+
+ghost
+fn assoc_hyp_r (#is: inames) (p q r s:slprop)
+   requires trade #is ((p ** q) ** r) s
+   ensures trade #is (p ** (q ** r)) s
+{
+  slprop_equivs ();
+  rewrite (trade #is ((p ** q) ** r) s) as (trade #is (p ** (q ** r)) s)
+}
+
+ghost
+fn assoc_concl_l (#is: inames) (p q r s:slprop)
+   requires trade #is p ((q ** r) ** s)
+   ensures trade #is p (q ** (r ** s))
+{
+  slprop_equivs ();
+  rewrite (trade #is p ((q ** r) ** s)) as (trade #is p (q ** (r ** s)))
+}
+
+ghost
+fn assoc_concl_r (#is: inames) (p q r s:slprop)
+   requires trade #is p (q ** (r ** s))
+   ensures trade #is p ((q ** r) ** s)
+{
+  slprop_equivs ();
+  rewrite (trade #is p (q ** (r ** s))) as (trade #is p ((q ** r) ** s))
+}
+
+ghost
+fn elim_hyp_l (#is: inames) (p q r:slprop)
+    requires (trade #is (p ** q) r) ** p
+    ensures (trade #is q r)
+{
+    curry _ _ _;
+    elim _ _;
+}
+
+ghost
+fn elim_hyp_r (#is: inames) (p q r:slprop)
+    requires (trade #is (p ** q) r) ** q
+    ensures (trade #is p r)
+{
+    comm_l _ _ _;
+    curry _ _ _;
+    elim _ _;
+}
+
+ghost
+fn reg_l
+  (#is : inames)
+  (p p1 p2: slprop)
+  requires (trade #is p1 p2)
+  ensures (trade #is (p ** p1) (p ** p2))
+{
+  ghost
+  fn aux
+    (_foo: unit)
+  requires ((trade #is p1 p2) ** (p ** p1))
+  ensures (p ** p2)
+  opens is
+  {
+    elim_trade #is p1 p2
+  };
+  intro_trade (p ** p1) (p ** p2) (trade #is p1 p2) aux
+}
+
+ghost
+fn reg_r
+  (#is: inames)
+  (p1 p2 p: slprop)
+  requires (trade #is p1 p2)
+  ensures (trade #is (p1 ** p) (p2 ** p))
+{
+  reg_l p p1 p2;
+  slprop_equivs ();
+  rewrite (trade #is (p ** p1) (p ** p2))
+    as (trade #is (p1 ** p) (p2 ** p))
+}
+
+ghost
+fn weak_concl_l
+  (#is: inames)
+  (p1 p2 p: slprop)
+  requires (trade #is p1 p2) ** p
+  ensures (trade #is p1 (p ** p2))
+{
+  ghost
+  fn aux
+    (_foo: unit)
+    requires ((trade #is p1 p2) ** p) ** p1
+    ensures p ** p2
+    opens is
+  {
+    elim_trade #is p1 p2
+  };
+  intro_trade p1 (p ** p2) ((trade #is p1 p2) ** p) aux
+}
+
+ghost
+fn weak_concl_r
+  (#is: inames)
+  (p1 p2 p: slprop)
+  requires (trade #is p1 p2) ** p
+  ensures (trade #is p1 (p2 ** p))
+{
+  weak_concl_l p1 p2 p;
+  slprop_equivs ();
+  refl' #is (p ** p2) (p2 ** p); // FIXME: why is the `is`  argument explicit?
+  trade_compose p1 _ _
+}
+
+ghost
+fn prod
+  (#is: inames)
+  (l1 r1 l2 r2: slprop)
+  requires (trade #is l1 r1 ** trade #is l2 r2)
+  ensures (trade #is (l1 ** l2) (r1 ** r2))
+{
+  ghost
+  fn aux
+    (_foo: unit)
+    requires ((trade #is l1 r1) ** (trade #is l2 r2)) ** (l1 ** l2)
+    ensures r1 ** r2
+    opens is
+  {
+    elim_trade #is l1 r1;
+    elim_trade #is l2 r2
+  };
+  intro_trade (l1 ** l2) (r1 ** r2) ((trade #is l1 r1) ** (trade #is l2 r2)) aux
+}
+
+ghost
+fn rewrite_with_trade_explicit
+//  (#[T.exact (`emp_inames)] is:inames) // FIXME: Pulse shouldn't remove this implicit marker
+  (is:inames)
+  (p1 p2: slprop)
+  requires p1 ** pure (p1 == p2)
+  ensures p2 ** (trade #is p2 p1)
+{
+  rewrite p1 as p2;
+  ghost
+  fn aux
+    (_: unit)
+    requires emp ** p2
+    ensures p1
+    opens is
+  {
+    rewrite p2 as p1
+  };
+  intro_trade _ _ _ aux
+}
+
+let rewrite_with_trade
+  (#[T.exact (`emp_inames)] is:inames)
+= rewrite_with_trade_explicit is
+
+ghost
+fn trans_hyp_l
+  (p1 p2 q r: slprop)
+requires
+  trade p1 p2 **
+  trade (p2 ** q) r
+ensures
+  trade (p1 ** q) r
+{
+  refl q;
+  prod p1 p2 q q;
+  trans _ _ r
+}
+
+ghost
+fn trans_hyp_r
+  (p q1 q2 r: slprop)
+requires
+  trade q1 q2 **
+  trade (p ** q2) r
+ensures
+  trade (p ** q1) r
+{
+  refl p;
+  prod p p q1 q2;
+  trans _ _ r
+}
+
+ghost
+fn trans_concl_l
+  (p q1 q2 r: slprop)
+requires
+  trade p (q1 ** r) **
+  trade q1 q2
+ensures
+  trade p (q2 ** r)
+{
+  refl r;
+  prod q1 q2 r r;
+  trans p _ _
+}
+
+ghost
+fn trans_concl_r
+  (p q r1 r2: slprop)
+requires
+  trade p (q ** r1) **
+  trade r1 r2
+ensures
+  trade p (q ** r2)
+{
+  refl q;
+  prod q q r1 r2;
+  trans p _ _
+}