Incorrect semantics for empty slice

[sanjit-bhat]

In Go, empty slices are different from nil slices. See this example.

However, GooseLang models empty slices as nil values.

perennial/src/goose_lang/lib/slice/impl.v

Lines 69 to 74 in 04f9b19

	Definition NewSlice (t: ty): val :=
	λ: "sz",
	if: "sz" = #0 then slice.nil
	else let: "cap" := make_cap "sz" in
	let: "p" := AllocN "cap" (zero_val t) in
	(Var "p", Var "sz", Var "cap").

[sanjit-bhat]

Concretely, in Perennial, I think we should be able to (faultily) prove this, whereas in Golang, this assertion fails.

func test() {
	slEmpt := make([]byte, 0)
	machine.Assert((slEmpt == nil) == true)
}

I'm not sure how to complete the proof. I got to WP impl.Assert ((slice.nil = slice.nil) = #true);; #() {{ v, Φ v }}. I think the slice.nil = slice.nil comparison should be a pure exec, but I'm struggling to get the system to recognize that.

[upamanyus]

Here's a way to prove it:

perennial/src/program_proof/bad_nil_slice.v

Lines 33 to 53 in 322c48d

	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.

[RalfJung]

Yeah, our NewSlice just returns null when the length is 0. I don't know if our memory even supports zero-sized allocations...

[upamanyus]

#72 (and its corresponding Goose changes) fixes this. Specifically, a nil gives (#null, #0, #0) while make([]T, 0) gives (#(Loc 1 0) +ₗ ArbitraryInt, #0, #0). The ArbitraryInt is there to model an arbitrary address, but it is technically only an offset within block 1. I couldn't think of a way to nondeterministically pick a block in the heap, but this should be good enough.