From b0e2d1e3f0eb3b9fa1f6f08be83496bc1b524c18 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Thu, 29 Dec 2022 14:46:13 -0500
Subject: [PATCH] Updated proof directory content listing in README.

---
 .../tasks/vTaskSwitchContext/proof/README.md  | 35 +++++++++++++++++--
 1 file changed, 32 insertions(+), 3 deletions(-)

diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md
index 96c791664..8d08e1e47 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md
@@ -6,11 +6,40 @@ This directory contains the bulk of VeriFast formalizations and proofs.
 
 # Directory Structure
 ```
-├── *.h files
-│   Headers containing VeriFast formalizations and proofs.
+├── lock_predicates.h
+│   Contains the formalization of the lock invariants, i.e., the invariants
+│   associated with: Masking interrupts, the task lock and the ISR lock.
+│   This file also contains the lemmas to prove that the task state updates
+│   in `prvSelectHighestPriorityTask` preserve the lock invariants.
 │
+├── port_contracts.h
+│   Contains VeriFast function contracts for macros with port-specific
+│   definitions, e.g., the macros to mask interrupts and to acquire AND
+│   release locks. These port-specific definitions often contain contain
+│   inline assembly VeriFast cannot reason about. The contracts allow us
+│   to abstract the semantics of the assembly.
+│
+├── ready_list_predicates.h
+│   Contains the predicates describing the ready lists as well as lemmas to
+│   reason about ready lists.
+│
+├── stack_predicates.h
+│   Contains the formalization of the stack layout used in the RP2040 port.
+│
+├── task_predicates.h
+│   Contains predicates describing task control blocks.
+│
+├── task_running_states.h
+│   `tasks.c` defines macros that are used to denote task run states.
+│   The proof headers in this directory cannot refer to these macros.
+│   This header contains auxiliary definitions used to expose the run state
+│   macros to the proof headers.
+│
+├── verifast_lists_extended.h
+│   Contains list axioms and lemmas that would naturally fit into VeriFast's
+│   standard list library `listex.gh`.
+│   
 ├── README.md
-│   Contains more details about the proof.
 │
 ├── single_core_proofs
 │   Contains the old list formalization and proofs written by