[hacspec] hacspec syntax

[Karthik Bhargavan]

Good question.

The reason we have bytes in there is that python has a native bytes type
with syntax for bytes literals.

However, I think it may be better to define bytes as an abbreviation of
array [uint8] and forego bytes literals. I will try to port the examples to
this style and see if it gets awkward for some reason

On Feb 12, 2018 03:49, "Bryan Parno" <parno at cmu.edu> wrote:

> This seems like an excellent initiative — thanks for getting it going!
>
> I’ll have to take a closer look at the examples, but I had a quick
> question: in the language description (https://github.com/HACS-
> workshop/hacspec/blob/master/LANGUAGE.md), why is `bytes` a special type,
> rather than being an array of uint8?
>
> Thanks,
> -Bryan
>
> On Feb 10, 2018, at 8:16 AM, 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 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/20180212/1ea653ec/attachment.html>