Advice on using RefinedC to verify List Copy
Apologies if this is the wrong place to address this query, and feel free to close/delete this issue if this is too off-topic.
I have been trying to use RefinedC to verify a simple instantiation of list-copy, but have been struggling to get the proofs to go through - at the moment however, I'm not sure if the issue is with my specification itself, or whether verifying the program in question is outside of RefinedC's capabilities.
The code being verified is as follows:
#include <stddef.h>
#include <stdbool.h>
#include <assert.h>
#include <refinedc.h>
#include "alloc.h"
typedef struct
[[rc::refined_by("s: {gmultiset nat}")]]
[[rc::ptr_type("list_t:"
"{s ≠ ∅} @ optional<&own<...>, null>")]]
[[rc::exists ("n: nat", "tail: {gmultiset nat}")]]
/* [[rc::size ("n")]] */
[[rc::constraints("{s = {[+n+]} ⊎ tail}")]]
list {
[[rc::field("n @ int<size_t>")]] size_t head;
[[rc::field("tail @ list_t")]] struct list* tail;
}* list_t;
[[rc::parameters("s: {gmultiset nat}", "r: loc", "x: loc")]]
[[rc::args("r @ &own<x @ &own<s @ list_t>>")]]
[[rc::requires("[alloc_initialized]")]]
[[rc::exists ("y: loc")]]
[[rc::ensures("own r : y @ &own<s @ list_t>", "own x : s @ list_t")]]
[[rc::tactics ("all: multiset_solver.")]]
void list_copy(list_t *r) {
list_t x = *r;
if(x == NULL) {
} else {
size_t v = x->head;
list_t nxt = x->tail;
*r = nxt;
list_copy(r);
list_t y1 = *r;
list_t y = alloc(sizeof(struct list));
y->tail = y1;
*r = y;
y->head = v;
}
}
The specifications have been adopted from the RefinedC paper (specifically the list definition is just a modification of the chunks list from the allocator in the paper), and the specification for list copy is trying to say that it should update the location r
to contain the copied list, while the function ensures that the original list is left unchanged. (The alloc function etc. is reusing the definitions/sources in the examples directory).
From my understanding of the paper, this should be a faithful transcription of my intended specification, but RefinedC fails to automatically verify this function.
I understand that the maintainers are all busy, and I apologise in advance for cluttering your issues with this slightly off-topic question. I would appreciate any advice you could spare.
Thanks.