Tighten TODO check to all directories

[achamayou]

We have had the check-todo script for a while now, as part of our executable project policy and it's done a good job of keeping tasks in issues, where they can be detailed, discussed and planned. Some directories had not been added at first, as we focused on the code we shipped, but we're not far off doing this across the project.

This change is a Draft for now, as a few things need to be cleaned up or converted into tickets, as the case may be.

[achamayou]

This is what's left now, after some clean up in #6180, #6179 and #6178. I'll do a pass today, and see what needs to be removed, what can be addressed, or what goes into tickets. If you'd like to claim some of these, feel free!

  tla/consensus/Traceccfraft.tla:179:    \* TODO Consider creating a mapping from clientRequests to actual values in the system trace.
  tla/consensus/Traceccfraft.tla:180:    \* TODO Alternatively, extract the written values from the system trace and redefine clientRequests at startup.
  tla/consensus/Traceccfraft.tla:211:\* TODO revisit this. See https://github.com/microsoft/CCF/pull/5988 for discussion.
  tla/consensus/Traceccfraft.tla:218:    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:233:    \* TODO /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
  tla/consensus/Traceccfraft.tla:235:    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:256:    \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
  tla/consensus/Traceccfraft.tla:258:    \*TODO /\ membershipState'[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state]
  tla/consensus/Traceccfraft.tla:259:    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:293:       \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
  tla/consensus/Traceccfraft.tla:296:       \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:328:    \*TODO /\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
  tla/consensus/Traceccfraft.tla:361:    \*TODO/\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
  tla/consensus/Traceccfraft.tla:363:    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:3[7](https://github.com/microsoft/CCF/actions/runs/9098846902/job/25010011336?pr=6177#step:5:9)4:       \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
  tla/consensus/Traceccfraft.tla:377:       \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:3[9](https://github.com/microsoft/CCF/actions/runs/9098846902/job/25010011336?pr=6177#step:5:11)5:    \*TODO/\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
  tla/consistency/Consistency.tla:274:\* TODO: Separate execution and response
  tla/consistency/ExternalHistoryInvars.tla:15:\* TODO: extend this to handle the fact that separate reads might get the same transaction ID
  tla/consistency/ExternalHistoryInvars.tla:172:\* TODO: Fix this definition (and related) as I am not quite happy with them
  tla/consistency/SingleNodeReads.tla:16:\* TODO: Separate execution and response

[achamayou]

Latest list after #6181

  tla/consensus/Traceccfraft.tla:179:    \* TODO Consider creating a mapping from clientRequests to actual values in the system trace.
  tla/consensus/Traceccfraft.tla:180:    \* TODO Alternatively, extract the written values from the system trace and redefine clientRequests at startup.
  tla/consensus/Traceccfraft.tla:211:\* TODO revisit this. See https://github.com/microsoft/CCF/pull/5988 for discussion.
  tla/consensus/Traceccfraft.tla:218:    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:233:    \* TODO /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
  tla/consensus/Traceccfraft.tla:235:    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:256:    \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
  tla/consensus/Traceccfraft.tla:258:    \*TODO /\ membershipState'[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state]
  tla/consensus/Traceccfraft.tla:259:    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:293:       \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
  tla/consensus/Traceccfraft.tla:296:       \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:328:    \*TODO /\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
  tla/consensus/Traceccfraft.tla:361:    \*TODO/\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
  tla/consensus/Traceccfraft.tla:363:    \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:3[7](https://github.com/microsoft/CCF/actions/runs/9113267281/job/25054344362?pr=6177#step:5:9)4:       \* TODO: /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
  tla/consensus/Traceccfraft.tla:377:       \*TODO/\ Len(log'[logline.msg.state.node_id]) = logline.msg.state.last_idx
  tla/consensus/Traceccfraft.tla:3[9](https://github.com/microsoft/CCF/actions/runs/9113267281/job/25054344362?pr=6177#step:5:11)5:    \*TODO/\ leadershipState'[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]