## The proof goal
```
(ensures ((fst (fieldPush_spec1 g st h_index wz 1UL)) ==
G.successor_push_itr1 (G.successors (create_graph_from_heap g) h_index)
(vl)
(st)
(0UL)))
```
### mark
`stack1 = fst (fieldPush_spec1 g st h_index wz 1UL)`
### dfs
`stack2 = G.successor_push_itr1 (G.successors (create_graph_from_heap g) h_index)
(vl)
(st)
(0UL)`
Hence to prove that `mark` and `dfs` creates the same stack, we need to prove `stack1 = stack2`. For that, the specification devised is as below, which works without difficulty as all `fields` are `pointers`. Hence the `successorlist` has same length as that of the iteration loop of `fieldPush`. Eventhough `fieldPush` is implemented as a recursive function, the loop effect is simulated with the help of the loop index variable `i` which represents the intermediate stage of an iteration.
### New specification need to be devised? Or can we still use the loop as `fieldPush` still iterates from `1UL` to `wz + 1`, where `i = wz + 1` is the exit condition of the loop
If the same loop framework is used, then the specification has to be tuned and new condition checks has top be introduces inside the loop of the lemma. This is because `length (successorlist) <= wz` when some field values are not pointers.
## Current Specification
```
(ensures ((fst (fieldPush_spec1 g st h_index wz i)) ==
G.successor_push_itr1 (G.successors (create_graph_from_heap g) h_index)
(vl)
(st)
(Usize.v i - 1)))
```
That is, a fieldPush starting at `h_index + 1 * mword` will produce the same stack as a `auccessorpush` starting at index `0`. This works since, each field is stored starting from index `0` of the `sucessor list`.
The same specification should hold when all field values are pointers as well as some field values are not pointers.
## Strategy to prove stack equivalence when all field values are pointers
let `object id = h_index`
Let `l = successor list of h_index`
Let `wz = wosize or number of fields of h_index`
Since all field values are object pointers,
`length l = wz `
### What `successorpush ()` in graph does?
`successorpush()` loops through `l` and checks each element whether it is unvisited (not member of stack or visited set). If, it pushes to the stack or else do nothing.
### What `fieldPush ()` does?
`fieldPush()` scans from `h_index + i * mword`, where `i` ranges from `1` to `wz + 1`. When `wz + 1` is hit., fieldPush exits. If `i < wz + 1`, then `(i-1) < wz`. Now we can together put the `successorpush ()` and `fieldPush()` in a recursive lemma where the base condition is `i == wz + 1`, where it simply returns the current stack. Since length of `successorlist` is `wz`, this way of proving does not pose an issue because `(i - 1)` is always less if it does not hit the base condition.
#### proof part
```
let i' = Usize.(i +^ 1UL) in
let grph = create_graph_from_heap g in
let l = G.successors grph h_index in
graph_successors_length_lemma g h_index;
graph_successors_mem_lemma g h_index;
assert (forall x. Seq.mem x l ==> Seq.mem x (get_allocated_block_addresses g));
assert (Seq.length l == Usize.v wz);
if Usize.v i = Usize.v wz + 1 then
(
let st_hp = (st,g) in
let st' = G.successor_push_itr1 l vl st (Usize.v i - 1) in
G.successor_push_itr1_lemma1 l vl st (Usize.v i - 1);
assert (st' == st);
assert (fst (fieldPush_spec1 g st h_index wz i) == st);
assert (G.successor_push_itr1 l vl st (Usize.v i - 1) == st);
()
)
else
(
let st', g' = fieldPush_spec_body g st h_index wz i in
assert (Usize.v i < Usize.v wz + 1);
arithmetic_lemma i wz;
assert (Usize.v i <= Usize.v wz);
arithmetic_lemma1 i wz;
assert (Usize.v i - 1 < Usize.v wz);
assert (Seq.length l == Usize.v wz);
assert (Usize.v i - 1 < Seq.length l);
let st'' = G.successor_push_body1 l vl st (Usize.v i - 1) in
fieldPush_spec_body_successor_push_body_equivalence_lemma1 g st h_index wz i vl;
assert (st' == st'');
fieldPush_spec_body_well_formed_allocated_blocks_lemma g st h_index wz i;
fieldPush_spec_body_graph_lemma g st h_index wz i;
assert (well_formed_allocated_blocks g');
fieldPush_spec1_well_formed_allocated_blocks_lemma g' st' h_index wz i';
let st1, g'' = fieldPush_spec1 g' st' h_index wz i' in
let st2 = G.successor_push_itr1 l vl st'' (Usize.v i - 1 + 1) in
let wz' = getWosize (read_word g' h_index) in
assert (wz == wz');
assert (objects2 0UL g == objects2 0UL g');
fieldPush_spec_body_valid_header_visited_set_lemma g st h_index wz i vl;
fieldPush_spec_body_black_nodes_visited_set_lemma g st h_index wz i vl;
assert (forall x. Seq.mem x vl ==> is_valid_header x g');
assert (forall x. Seq.mem x (objects2 0UL g') /\ isBlackObject1 x g' <==> Seq.mem x vl);
fieldPush_spec_successor_push_itr_equivalence_lemma1 g' st' h_index wz i' vl;
assert (st1 == st2);
assert (fst (fieldPush_spec1 g' st' h_index wz i') == st2);
assert (fst (fieldPush_spec1 g' st' h_index wz i') == G.successor_push_itr1 l vl st'' (Usize.v i - 1 + 1));
fieldPush_fieldPush_spec_body_lemma g st h_index wz i i';
assert (fieldPush_spec1 g st h_index wz i == fieldPush_spec1 (snd (fieldPush_spec_body g st h_index wz i))
(fst (fieldPush_spec_body g st h_index wz i))
h_index
wz
i');
assert (fieldPush_spec1 g st h_index wz i == fieldPush_spec1 g' st' h_index wz i');
G.successor_push_itr1_lemma l vl st (Usize.v i - 1);
assert ((fst (fieldPush_spec1 g st h_index wz i)) == G.successor_push_itr1 (G.successors (create_graph_from_heap g) h_index)
(vl)
(st)
(Usize.v i - 1));
()
)
```
## Problem with this approcah when some field values are not pointers
```
length l <= wz
```
So we cannot call a lemma that together iterates over `successorlist` and field values as we cannot prove, `(i-1) < wz`.
## New strategy
fieldpush from 1ul to wz on st should create the same st' as successorpush from 0ul to (length successorlist - 1).
input stack - same
suppose outputs are as follows:
`fieldpush - st1`
successorpush - st2
```
st1 = st ++ white pointer fields of object with id hindex.
st1 = st ++ w1
```
`st2 = st ++ unvisited successors from successor list of object with id hindex`
unvisited successor = not in stack and not in vl --> not grey and not black. Since all successors are members of allocated blocks, unvisited successors should be white in color.
```
st2 = st ++ white successors
st2 = st ++ w2
```
prove that `w1 == w2`
`fieldaddrs set`
`heap, h`
```
fieldobjects = h[fieldaddrs in order]
white objects = h[fieldsddrs in order]
```
## Suggestion [KN]
We can define functions ```get_succ_h heap node i``` and ```get_succ_g graph node i``` which output the list of successors of node in the heap and graph respectively, beginning from index i. During graph creation, we can show the following:
```
get_succ_h heap node 1 == get_succ_g graph node 0
```
Now, the specification of fieldPush can be changed to following:
```
(requires (get_succ_h heap node i == get_succ_g graph node j))
```
```
(ensures ((fst (fieldPush_spec1 g st h_index wz i)) ==
G.successor_push_itr1 (G.successors (create_graph_from_heap g) h_index)
(vl)
(st)
j))
```
The same requires clause can also be added to fieldPush_body.
stack equivalence proof for mword_plus_pointer is completed. I used the strategy suggested by Kartik sir. Created two functions and 23 lemmas. The main lemma proof is complex with two branches and within the second branch, three more branches. This captures the various situations between the successor_push in a graph and a fieldPush in a heap, when some field values are not pointers. All changes are pushed into github and added comments for easy reading. Total lines of code for this effort is 1570 lines.
https://github.com/prismlab/verified-gc/blob/4be44278587655f51971cefa4ee222b450381ef7/OCaml_GC/mword_plus_pointer/Spec.GC7.fsti#L6524
Sign in with Wallet
Connect another wallet