Commit c0ffc3f9 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Renaming [block_id] into [label].

Using [block_id] to refer to the first component of locations.
parent 5552a911
Pipeline #36172 passed with stage
in 31 minutes and 57 seconds
......@@ -31,9 +31,9 @@ Section proof_btree_member.
m !! k = cur_m !! k
]> $
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "btree_member" "#0".
- repeat liRStep; liShow.
......
......@@ -18,9 +18,9 @@ Section proof_free_btree.
start_function "free_btree" ([]) => arg_t.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "free_btree" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -25,9 +25,9 @@ Section proof_key_index.
s length l
]> $
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "key_index" "#0".
- repeat liRStep; liShow.
......
......@@ -17,9 +17,9 @@ Section proof_new_btree.
start_function "new_btree" ([]) => local_t.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "new_btree" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -15,9 +15,9 @@ Section proof_latch_release.
start_function "latch_release" ([[p beta] P]) => arg_latch.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "latch_release" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -18,9 +18,9 @@ Section proof_latch_wait.
arg_latch ◁ₗ (p @ (&frac{beta} (latch (P))))
]> $
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "latch_wait" "#0".
- repeat liRStep; liShow.
......
......@@ -18,9 +18,9 @@ Section proof_increment.
start_function "increment" ([[[[p q] n1] n2] n3]) => arg_t local_ret.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "increment" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -17,9 +17,9 @@ Section proof_init.
start_function "init" (p) => arg_t.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "init" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -18,9 +18,9 @@ Section proof_read_locked.
start_function "read_locked" ([[[[p q] n1] n2] n3]) => arg_t local_ret.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "read_locked" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -16,9 +16,9 @@ Section proof_read_outside.
start_function "read_outside" ([[[p n1] n2] n3]) => arg_t.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "read_outside" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -18,9 +18,9 @@ Section proof_write_locked.
start_function "write_locked" ([[[[[p n] q] n1] n2] n3]) => arg_t arg_n.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "write_locked" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -16,9 +16,9 @@ Section proof_write_outside.
start_function "write_outside" ([[[[p n] n1] n2] n3]) => arg_t arg_n.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "write_outside" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -14,9 +14,9 @@ Section proof_slab_alloc.
start_function "slab_alloc" ([[p n] entry_size]) => arg_s local_r local_f.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "slab_alloc" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -14,9 +14,9 @@ Section proof_slab_free.
start_function "slab_free" ([[[p fp] n] entry_size]) => arg_s arg_x local_f.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "slab_free" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -14,9 +14,9 @@ Section proof_slab_init.
start_function "slab_init" ([[[p chunk_p] n] entry_size]) => arg_s arg_p arg_chunksize arg_entry_size.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "slab_init" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -18,9 +18,9 @@ Section proof_mpool_add_chunk.
start_function "mpool_add_chunk" ([[[[p q] n] entry_size] m]) => arg_p arg_begin arg_size local_chunk.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "mpool_add_chunk" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -25,9 +25,9 @@ Section proof_mpool_alloc.
q = Own n = 0%nat
]> $
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "mpool_alloc" "#0".
- repeat liRStep; liShow.
......
......@@ -28,9 +28,9 @@ Section proof_mpool_alloc_contiguous.
q = Own n2 <= n
]> $
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "mpool_alloc_contiguous" "#0".
- repeat liRStep; liShow.
......
......@@ -19,7 +19,7 @@ Section proof_mpool_alloc_contiguous_no_fallback.
start_function "mpool_alloc_contiguous_no_fallback" ([[[[[p q] n] entry_size] count] align]) => arg_p arg_count arg_align local_prev local_before_start local_chunk_next local_new_chunk local_start local_ret local_chunk_size local_chunk.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
<[ "#1" :=
pc : loc,
entries_in_chunks1 : nat,
......@@ -40,7 +40,7 @@ Section proof_mpool_alloc_contiguous_no_fallback.
shelve_hint (q = Own n = (entries_in_chunks1 + entries_in_chunks2 + entries_in_entry_list)%nat)
]> $
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "mpool_alloc_contiguous_no_fallback" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
......@@ -18,9 +18,9 @@ Section proof_mpool_alloc_no_fallback.
start_function "mpool_alloc_no_fallback" ([[[p q] n] entry_size]) => arg_p local_new_chunk local_entry local_ret local_chunk.
split_blocks ((
)%I : gmap block_id (iProp Σ)) ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap block_id (iProp Σ)).
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "mpool_alloc_no_fallback" "#0".
Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment