Buggy example of nil vs empty slice

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.