GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

allow property annotation to encompass a block of properties #1622

Open weaversa opened 9 months ago

weaversa commented 9 months ago

This is a request for feedback on making the property keyword handle blocks of properties. So, it would essentially scope similar the current private annotation. I don't think this breaks any current specifications using the property annotation, and provides a bit more flexibility towards expressing properties. If there is concern that this would be a breaking change, a properties annotation could be used for blocks of properties.

...
// Declare some properties
property
  myproperty : Bit
  myproperty = True

  anotherproperty : Integer -> Bit
  anotherproperty = x + x == x * 2

// Back to functions
function1 x = x + 10
...
sauclovian-g commented 9 months ago

See #331