From 18b8bfcf2904242952ddb9c9cf2e7d1e6c19511c Mon Sep 17 00:00:00 2001 From: Johannes Hostert <jhostert@ethz.ch> Date: Wed, 19 Mar 2025 08:26:33 +0100 Subject: [PATCH] update README --- theories/tree_borrows/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md index 9ea165f6..331e216c 100644 --- a/theories/tree_borrows/README.md +++ b/theories/tree_borrows/README.md @@ -82,12 +82,12 @@ A retag is the core operation creating a new reference, which is parameterized b Further it defines whether there are to be protectors. The function `create_child` is the main function used during a retag. -Finally, the protector end semantics are defined starting at lien 841, with the function `tree_get_all_protected_tags_initialized_locs` and `tree_access_all_protected_initialized`. +Finally, the protector end semantics are defined starting at line 841, with the functions `tree_get_all_protected_tags_initialized_locs` and `tree_access_all_protected_initialized`. To put all the definitions together, the inductive `bor_step` is defined. It is coupled to the main operational semantics by a series of "events". For example, a read (called "copy" here) causes a `CopyEvt`, which is picked up by the `CopyIS` rule. -This will ensure the tag exists, and then cause a read event. +This will ensure the tag exists, and then traverse the tree, advancing the state machine appropiately and triggering UB if necessary. Also of interests to reviewers are lines 1000-1038. This defines a "unit test" for the `rel_dec` and `create_child` functions. Since `rel_dec` is not commutative, it can be difficult to remember which node is which and whether an output of e.g. "Child" means that the first node is a child of the second or the other way around. -- GitLab