Remove unused slice capacity and add new function that returns pointer for queue tutorial.

This will make proofs easier by proving a function that directly returns a pointer which will have a spec and proof that do the work of initializing all of the ghost state. Also the capacity here is unused. It seems like the idea was to make the slice fixed length but in reality the capacity is only used in Go slices to determine when to upsize and in this case since the initial size is queue_size it actually has no effect. This will be followed by updates to goose code and proofs.

Author: lredlin

tutorial/queue/queue.go

@@ -15,7 +15,18 @@ type Queue struct {
 func NewQueue(queue_size uint64) Queue {
 	lock := new(sync.Mutex)
 	return Queue{
-		queue: make([]uint64, queue_size, queue_size),
+		queue: make([]uint64, queue_size),
+		cond:  sync.NewCond(lock),
+		lock:  lock,
+		first: 0,
+		count: 0,
+	}
+}
+
+func NewQueueRef(queue_size uint64) *Queue {
+	lock := new(sync.Mutex)
+	return &Queue{
+		queue: make([]uint64, queue_size),
 		cond:  sync.NewCond(lock),
 		lock:  lock,
 		first: 0,