From f15540ceccfe979289f802fecefbb40628523675 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Wed, 28 Dec 2022 10:36:17 -0500 Subject: [PATCH] Handled minor TODOs in proof headers. --- .../custom_build_scripts_RP2040/vf_rewrite.sh | 3 +- .../tasks/vTaskSwitchContext/include/list.h | 3 - .../vTaskSwitchContext/include/stack_macros.h | 2 - .../vTaskSwitchContext/proof/port_contracts.h | 3 - .../proof/ready_list_predicates.h | 2 +- .../scp_list_predicates_extended.h | 4 +- .../proof/verifast_lists_extended.h | 65 +------------------ 7 files changed, 6 insertions(+), 76 deletions(-) diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/vf_rewrite.sh b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/vf_rewrite.sh index 81e3a5b41..8408ab8b1 100755 --- a/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/vf_rewrite.sh +++ b/Test/VeriFast/tasks/vTaskSwitchContext/custom_build_scripts_RP2040/vf_rewrite.sh @@ -39,9 +39,8 @@ echo "Delete fixed-sized array typedefs" rewrite "typedef .*\[[0-9]*\];" "" echo "Delete attributes" -#rewrite "\_\_attribute\_\_\(\(\_\_[a-z\_]*\_\_\)\)" "" rewrite "__attribute__(([_a-z]*))" "" -# TODO: Why does matching `\s` or `:space:` not work on MacOs? +# Note: `\s` or `:space:` not work on MacOs. rewrite "__attribute__( ( [_a-z]* ) )" "" echo "Delete void casts (used to suppress compiler warnings)" diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/include/list.h b/Test/VeriFast/tasks/vTaskSwitchContext/include/list.h index d1543dfed..5a19ba019 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/include/list.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/include/list.h @@ -80,9 +80,6 @@ * numbers of tokens when expanding `PRIVILEGED_FUNCTION` in this file. */ #define PRIVILEGED_FUNCTION - // TODO: Figure out why the preprocessors consume different amounts of - // of tokens. This most likely has to do with the path/context - // from which this header is included. #endif /* VERIFAST */ /* diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h b/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h index e0162f57a..51af7925b 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h @@ -84,8 +84,6 @@ #if ( ( configCHECK_FOR_STACK_OVERFLOW > 1 ) && ( portSTACK_GROWTH < 0 ) ) - /* TODO: Convert this macro into a function such that we can insert proof annotations. - */ #ifdef VERIFAST /* Reason for rewrite: * VeriFast complains about unspecified evaluation order of diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h index eedbca87f..a72b57597 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h @@ -3,9 +3,6 @@ // We want our proofs to hold for an arbitrary number of cores. -/* TODO: Can we use the original function `get_core_num` instead without - * adding the contract inside the pico sdk file (platform.h)? - */ #undef portGET_CORE_ID #define portGET_CORE_ID() VF__get_core_num() diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h index 41a04b484..bb22ab5d0 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h @@ -320,7 +320,7 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem) //@ assert( forall(gOwners, (mem_list_elem)(gTasks)) == true ); //@ forall_remove_nth(index_of(pxTaskItem, gCells), gOwners, (mem_list_elem)(gTasks)); //@ assert( forall(gOwners2, (mem_list_elem)(gTasks)) == true ); - //@ forall_mem_implies_subset(gOwners2, gTasks); + //@ forall_mem_implies_superset(gTasks, gOwners2); //@ assert( subset(gOwners2, gTasks) == true ); vListInsertEnd( pxReadyList, pxTaskItem ); diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs_extended/scp_list_predicates_extended.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs_extended/scp_list_predicates_extended.h index 48e9afb0f..950c5475a 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs_extended/scp_list_predicates_extended.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/single_core_proofs_extended/scp_list_predicates_extended.h @@ -239,8 +239,8 @@ ensures assert( gValsRes == append(gValsPrefix, cons(gItemVal, nil)) ); - drop_cons(gCells, index_of(pxItem, gCells)); - drop_cons(gVals, index_of(pxItem, gCells)); + drop_n_plus_one(gCells, index_of(pxItem, gCells)); + drop_n_plus_one(gVals, index_of(pxItem, gCells)); nth_index(gCells, pxItem); assert( gCellsRes == gCells ); diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h index 43c6be5aa..62f8e4e9a 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h @@ -5,55 +5,30 @@ * of VeriFast's standard library. */ +// Most of the following lemmas are axioms. - -// TODO: Can we prove this in VeriFast or do we have to axiomatise? /*@ lemma void head_drop_n_equals_nths(list xs, int n); requires n >= 0; ensures head(drop(n, xs)) == nth(n, xs); -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void drop_index_equals_singleton_implies_last_element(list xs, t x); requires drop(index_of(x, xs), xs) == cons(x, nil); ensures index_of(x, xs) == length(xs) - 1; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? -// Can we replace this by standard lemma `drop_n_plus_one`? -lemma void drop_cons(list xs, int n); -requires n < length(xs); -ensures drop(n, xs) == cons(nth(n, xs), drop(n+1, xs)); - -// TODO: Can we prove this in VeriFast or do we have to axiomatise? -lemma void nth_index(list xs, t x) +lemma void nth_index(list xs, t x); requires mem(x, xs) == true; ensures nth(index_of(x, xs), xs) == x; -{ - // Will prove later. For now, we only validate with an example. - list _xs = cons(1, cons(2, cons(3, cons(4, cons(5, cons(6, cons(7, nil))))))); - int _x = 4; - int i = index_of(_x, _xs); - int nthi = nth(index_of(_x, _xs), _xs); - - assert( nth(index_of(_x, _xs), _xs) == _x ); - - // ADMIT LEMMA, PROVE LATER - assume(false); -} - -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void mem_prefix_implies_mem(t x, list xs, int n); requires mem(x, take(n, xs)) == true; ensures mem(x, xs) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void mem_suffix_implies_mem(t x, list xs, int n); requires mem(x, drop(n, xs)) == true; ensures mem(x, xs) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void drop_n_plus_m(list xs, int n, int m); requires true; ensures drop(n, drop(m, xs)) == drop(n + m, xs); @@ -78,7 +53,6 @@ fixpoint bool superset(list super, list sub) { } -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void update_out_of_bounds(int index, t x, list xs) requires (index < 0 || index >= length(xs)); ensures update(index, x, xs) == xs; @@ -91,7 +65,6 @@ ensures update(index, x, xs) == xs; } } - lemma void index_of_different(t x1, t x2, list xs) requires x1 != x2 &*& mem(x1, xs) == true &*& mem(x2, xs) == true; ensures index_of(x1, xs) != index_of(x2, xs); @@ -105,91 +78,57 @@ ensures index_of(x1, xs) != index_of(x2, xs); } } -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void subset_cons_tail(list xs); requires xs == cons(?h, ?t); ensures subset(t, xs) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void remove_result_subset(t x, list xs); requires true; ensures subset(remove(x, xs), xs) == true; -// TODO: Revisit this lemma -// { -// switch(xs) { -// case nil: -// case cons(h, t): -// remove_result_subset(x, t); -// if(h == x) { -// assert( remove(x, xs) == t ); -// subset_cons_tail(xs); -// assert( subset(t, cons(x, t) ) == true ); -// } else { -// ; -// } -// } -// } -// TODO: Can we prove this in VeriFast or do we have to axiomatise? // Special case of `nth_update` from `listex.gh`. lemma void update_preserves_rest(int i, int u, t v, list xs); requires 0 <= i && i < length(xs) && 0 <= u && u < length(xs) && i != u; ensures nth(i, update(u, v, xs)) == nth(i, xs); -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void append_take_nth_drop(int n, list xs); requires 0 <= n &*& n < length(xs); ensures xs == append( take(n, xs), cons(nth(n, xs), drop(n+1, xs)) ); -// TODO: Can we prove this in VeriFast or do we have to axiomatise? // Note: `listex.gh` contains lemma `forall_drop` but no corresponding // `forall_take`. lemma void forall_take(list xs, fixpoint(t, bool) p, int i); requires forall(xs, p) == true; ensures forall(take(i, xs), p) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void forall_mem_implies_superset(list super, list sub); requires forall(sub, (mem_list_elem)(super)) == true; ensures superset(super, sub) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? -// TODO: Rename into "forall_mem_implies_superset" -lemma void forall_mem_implies_subset(list sub, list super); -requires forall(sub, (mem_list_elem)(super)) == true; -ensures superset(super, sub) == true; - -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void subset_implies_forall_mem(list sub, list super); requires subset(sub, super) == true; ensures forall(sub, (mem_list_elem)(super)) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void forall_remove(t x, list xs, fixpoint(t, bool) p); requires forall(xs, p) == true; ensures forall(remove(x, xs), p) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void forall_remove_nth(int n, list xs, fixpoint(t, bool) p); requires forall(xs, p) == true; ensures forall(remove_nth(n, xs), p) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void nth_implies_mem(int n, list xs); requires 0 <= n &*& n < length(xs); ensures mem(nth(n, xs), xs) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void subset_append(list sub1, list sub2, list super); requires subset(sub1, super) == true &*& subset(sub2, super) == true; ensures subset(append(sub1, sub2), super) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void subset_take(int i, list xs); requires true; ensures subset(take(i, xs), xs) == true; -// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void subset_drop(int i, list xs); requires true; ensures subset(drop(i, xs), xs) == true;