[hacspec] hacspec syntax

[Karthikeyan Bhargavan]

Hello All,

It would be great to get some opinions on the hacspec syntax, types, and semantics.

At HACS, we started with cryptol as the initial language (which makes great sense considering the tool support.)
On the hackathon day, the group moved towards a subset of python, since developers/spec authors already use it as pseudocode in RFCs.

For now, we have identified a small subset of python, with static types checked with mypy.
We have written some specs in this subset in /specs and we believe this subset is adequate to write idiomatic specifications for most of the primitives currently in /formal-models.
I believe this syntax can be compiled to idiomatic Cryptol and F*, but we need to see how they translate to other formalisms.

As time goes along, we can add more constructs as needed, but let me informally describe the current features and the open questions:

INTEGERS:
	The language includes arbitrary precision integers (int), and fixed-size integers (uint8, uint32, uint64, uint128; we can add more as needed.)
	Standard arithmetic operators are overloaded over these integer types, and arithmetic overflows are treated with a wrapping semantics.
TUPLES (RECORDS?):
	You can build and pass around tuples of values (Tuple[T1,…,Tn])
	We have not included records yet, but we could, if desired, include JSON-like dictionaries (see the files in /test-vectors)
ARRAYS:
	The only other data structures currently are arrays of fixed-length (array[T]).
	You can read and write arrays, and you can read and write slices from arrays.
	You can filter an array or apply a function to each element using array comprehensions (like in Python).
	You can split an array into blocks and you can concatenate these blocks back into a flat array.
	We are uncertain whether to include higher-order operators like map and reduce or to rely on comprehensions and for-loops instead
LOOPS:
	The only looping construct is a for loop over a range.
	If need be, we can add other looping constructs or recursion.
SIDE-EFFECTS (?):
	Variables and arrays in the language can be modified, however we would like to limit all side-effects to local variables within functions.
	Functions always return their outputs, they do not modify any of their arguments.
	When arrays are passed into and out of functions, they are effectively copied in and copied out.
	This part of the semantics needs some thinking and discussion to find a good middle-ground,
	since the python syntax is naturally imperative, but most of the formal models we have looked
	at find it easier to reason about purely functional specificaion.

I am sure there is much else to look at and think about, but comments on the above would already be a good start.

Best regards,
Karthik




-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180210/4b837c6a/attachment.sig>