project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
120 stars 20 forks source link

Reading let/delay should not require counting positions within tuples #874

Open samuelgruetter opened 2 years ago

samuelgruetter commented 2 years ago

Currently, let/delay expressions typically look like this:

let/delay '(st1, st2, ... stN) :=
  let tmp1 := ... in
  let tmp2 := ... in
  ...
  let tmpM := ... in
  (new_st1, new_st2, ... new_stN)
  initially (init_st1, init_st2, ..., init_stN)
in
  rest

I find these hard to read because the tuple (st1, st2, ... stN) is quite far away from the tuple (new_st1, new_st2, ... new_stN) that gets assigned to it, and to know which state variable st gets assigned which new_st, I have to determine and compare their position within the tuple, which is not very convenient. The same problem occurs when trying to determine the initial value of each st.

I would find it better to have a syntax where the initial value and the updated value of each state variable are next to the name of the state variable, eg like this:

let/delay
  st1 := new_st1 initially init_st1;
  st2 := new_st2 initially init_st2;
  ...
  stN := new_stN initially init_stN;
where
  tmp1 := ...;
  tmp2 := ...;
  ...
  tmpM := ...;
in
  rest

Should we try to implement a notation similar to this one?

blaxill commented 2 years ago

Yeah I think this could be a good change. Perhaps let/delay b1 := e1 and b2 := e2 ... in ... or something might be closer to OCaml? I agree the distance+tupling is not clear right now.