From 322c48d10a00cd6d8a05a77176ea2da46a22a5ce Mon Sep 17 00:00:00 2001
From: Upamanyu Sharma <upamanyu@mit.edu>
Date: Mon, 11 Mar 2024 22:59:45 -0400
Subject: [PATCH] Buggy example of nil vs empty slice

---
 src/program_proof/bad_nil_slice.v | 55 +++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 src/program_proof/bad_nil_slice.v

diff --git a/src/program_proof/bad_nil_slice.v b/src/program_proof/bad_nil_slice.v
new file mode 100644
index 000000000..7f425fcdd
--- /dev/null
+++ b/src/program_proof/bad_nil_slice.v
@@ -0,0 +1,55 @@
+(*
+package test
+
+import (
+    "github.com/tchajed/goose/machine"
+)
+
+func test() {
+	slEmpt := make([]byte, 0)
+	machine.Assert((slEmpt == nil) == true)
+}
+*)
+(* autogenerated from test *)
+From Perennial.goose_lang Require Import prelude.
+
+Section code.
+Context `{ext_ty: ext_types}.
+Local Coercion Var' s: expr := Var s.
+
+(* FIXME: should not be possible to prove this assert *)
+Definition test: val :=
+  rec: "test" <> :=
+    let: "slEmpt" := NewSlice byteT #0 in
+    control.impl.Assert (("slEmpt" = slice.nil) = #true);;
+    #().
+
+End code.
+
+From Perennial.program_proof Require Import grove_prelude.
+From Perennial.goose_lang.lib Require Import slice.
+Section proof.
+Context `{!heapGS Σ}.
+Lemma wp_test :
+  {{{
+        True
+  }}}
+    test #()
+  {{{
+        RET #(); True
+  }}}
+.
+Proof.
+  iIntros (Φ) "_ HΦ".
+  wp_lam. wp_pures.
+  rewrite /NewSlice.
+  rewrite /slice.nil.
+  wp_pures.
+  wp_pure1.
+  { done. }
+  wp_apply wp_Assert.
+  2:{ wp_pures; by iApply "HΦ". }
+  done.
+Qed.
+
+End proof.