Both tree_remove and tree_remove_helper are complete and precise, but tree_remove_lemma_left is imprecise. When looking at the code with runtime checks inserted, tree_remove_lemma_left is being passed an empty OwnedFields struct; we aren’t doing anything to recreate the permissions at the call site, so the first runtime check in tree_remove_lemma_left fails immediately. The precondition for tree_remove_lemma_left is:
//@requires ? && bst(l, min, max) && max < x;
So we should be adding the permissions for bst to OwnedFields.
To recreate this issue, verify the included partial spec and run with workload 2, or directly compile the checked version, which has the correct workload value hard coded. Line numbers in the trace above refer to the checked version/verifier output.
Running the checked partial spec #156/157 of BST at workload 2 leads to the following trace:
Both
tree_removeandtree_remove_helperare complete and precise, buttree_remove_lemma_leftis imprecise. When looking at the code with runtime checks inserted,tree_remove_lemma_leftis being passed an empty OwnedFields struct; we aren’t doing anything to recreate the permissions at the call site, so the first runtime check intree_remove_lemma_leftfails immediately. The precondition fortree_remove_lemma_leftis:So we should be adding the permissions for
bstto OwnedFields. To recreate this issue, verify the included partial spec and run with workload 2, or directly compile the checked version, which has the correct workload value hard coded. Line numbers in the trace above refer to the checked version/verifier output.