[hacspec] hacspec syntax

Tue Feb 13 00:00:45 PST 2018

>
> Seems a bit simplistic?
>

Sure, this was meant to show how we could add pre/post conditions easily to
hacspec with valid python. This precondition and the way it's evaluated is
too simplistic to be useful. But it can be extended to do something
meaningful.
That said we're at a point where we might want to write our own type
checker for the subset of python hacspec is using as we hit many
limitations of mypy right now.

On Mon, Feb 12, 2018 at 11:33 AM, Ben Laurie <benl at google.com> wrote:

>
>
> On 11 February 2018 at 19:21, Franziskus Kiefer <
> franziskuskiefer at gmail.com> wrote:
>
>> This brings up a question: should we introduce general refinement types?
>>>> E.g. poly1305_field = x:int{x >= 0 && x < 2**130 - 5}
>>>>
>>>
>>> If it has to be true, we should have a way to express it?
>>>
>>> Pre- and post- conditions?
>>>
>>
>> Having pre/post conditions would be great and maybe easier to do.
>> We could write simple decorators in speclib for pre and post conditions.
>> I added a simple precondition to chacha20 [1] checking that the counter
>> is positive. The precondition decorator is implemented in speclib [2].
>> This is not great yet, but could be a way to add pre- and post-conditions.
>>
>> Cheers,
>> Franziskus
>>
>> [1] https://github.com/HACS-workshop/hacspec/blob/master/specs/
>> chacha20.py#L59
>> [2] https://github.com/HACS-workshop/hacspec/blob/master/specs/
>> speclib.py#L302
>>
>
> Seems a bit simplistic?
>
>
>>
>>
>>
>>
>> On Sat, Feb 10, 2018 at 9:15 PM, Ben Laurie <benl at google.com> wrote:
>>
>>>
>>>
>>> On 10 February 2018 at 17:41, Karthikeyan Bhargavan <
>>> karthik.bhargavan at gmail.com> wrote:
>>>
>>>>
>>>> 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?
>>>>
>>>>
>>>> This is a good point and shows up the limitations of the current
>>>> python-based type system.
>>>> Since we are working in a subset of python and are typechecking our
>>>> code via mypy,
>>>> we cannot currently state or check sizes of types.
>>>>
>>>> This brings up a question: should we introduce general refinement types?
>>>> E.g. poly1305_field = x:int{x >= 0 && x < 2**130 - 5}
>>>>
>>>
>>> If it has to be true, we should have a way to express it?
>>>
>>> Pre- and post- conditions?
>>>
>>>
>>>>
>>>> Or at the very least, should we add length annotations a la rust?
>>>> E.g. chacha20_state = array[uint32; 16]
>>>>
>>>> If we want to stay within Python, we would ned to hide such annotations
>>>> within comments.
>>>> The benefit of sticking within Python syntax is that the code is
>>>> immediately executable without any preprocessing.
>>>> However, if the syntax starts getting awkward, we should be open to
>>>> adding a “light” erasure step that throws away some annotations.
>>>>
>>>> Also, in the ctr.py example, is that assuming msg is some multiple of
>>>> the block size?
>>>>
>>>>
>>>> In counter_mode(), msg has an arbitrary size.
>>>> In block_encrypt() msg has size <= blocksize.
>>>>
>>>> If msg < blocksize, then zip(keyblock,msg) truncates the result to the
>>>> shorter length.
>>>> I realize this is confusing and undocumented, and I’ll try to rewrite
>>>> this.
>>>>
>>>
>>> Zipping with an explanation is fine.
>>>
>>>
>>>>
>>>>
>>>> We're using LIONESS at work, which is only loosely specified, and we
>>>> were thinking of writing a hacspec spec for it…
>>>>
>>>>
>>>> That would be great. I am trying to get my students to write specs for
>>>> Curve25519, SHA-2, AES, etc. but getting a diverse set of specs will shake
>>>> out the syntax.
>>>>
>>>> -Karthik
>>>>
>>>>
>>>>
>>>>
>>>>> 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
>>>>
>>>>
>>>>
>>>
>>> _______________________________________________
>>> 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/20180213/e0d997b8/attachment.html>