[hacspec] hacspec syntax

[Ben Laurie]

On 10 February 2018 at 13:16, Karthikeyan Bhargavan <
karthik.bhargavan at gmail.com> wrote:

> 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 was looking at those today, and I'm a bit confused - it doesn't seem
possible to specify the sizes of int and bytes types?

Also, in the ctr.py example, is that assuming msg is some multiple of the
block size?

We're using LIONESS at work, which is only loosely specified, and we were
thinking of writing a hacspec spec for it...



> 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
>
>
>
>
>
> _______________________________________________
> Hacspec mailing list
> Hacspec at moderncrypto.org
> https://moderncrypto.org/mailman/listinfo/hacspec
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180210/96b5456e/attachment.html>