<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>Seems a bit simplistic?</div></blockquote><div><br></div><div>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.</div><div>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.<br></div><div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 12, 2018 at 11:33 AM, Ben Laurie <span dir="ltr"><<a href="mailto:benl@google.com" target="_blank">benl@google.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote"><span class="">On 11 February 2018 at 19:21, Franziskus Kiefer <span dir="ltr"><<a href="mailto:franziskuskiefer@gmail.com" target="_blank">franziskuskiefer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><span><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <span class="m_6809180135575754821m_6444996775725113078gmail-im"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div><div>This brings up a question: should we introduce general refinement types?</div><div>E.g. poly1305_field = x:int{x >= 0 && x < 2**130 - 5}</div></div></div></blockquote><div><br></div></span><div>If it has to be true, we should have a way to express it?</div><div><br></div><div>Pre- and post- conditions?</div></blockquote><div><br></div></span><div>Having pre/post conditions would be great and maybe easier to do.<br></div><div>We could write simple decorators in speclib for pre and post conditions.</div><div>I added a simple precondition to chacha20 [1] checking that the counter is positive. The precondition decorator is implemented in speclib [2].</div><div>This is not great yet, but could be a way to add pre- and post-conditions.</div><div><br></div><div>Cheers,</div><div>Franziskus<br></div><div><br></div><div>[1] <a href="https://github.com/HACS-workshop/hacspec/blob/master/specs/chacha20.py#L59" target="_blank">https://github.com/HACS-worksh<wbr>op/hacspec/blob/master/specs/<wbr>chacha20.py#L59</a></div><div>[2] <a href="https://github.com/HACS-workshop/hacspec/blob/master/specs/speclib.py#L302" target="_blank">https://github.com/HACS-worksh<wbr>op/hacspec/blob/master/specs/<wbr>speclib.py#L302</a></div></div></blockquote><div><br></div></span><div>Seems a bit simplistic?</div><div><div class="h5"><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><br></div><div><br></div><div><div> </div></div></div><div class="m_6809180135575754821HOEnZb"><div class="m_6809180135575754821h5"><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Feb 10, 2018 at 9:15 PM, Ben Laurie <span dir="ltr"><<a href="mailto:benl@google.com" target="_blank">benl@google.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote"><span>On 10 February 2018 at 17:41, Karthikeyan Bhargavan <span dir="ltr"><<a href="mailto:karthik.bhargavan@gmail.com" target="_blank">karthik.bhargavan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><br><div><span><blockquote type="cite"><div><div class="gmail_quote" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><div>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?</div></div></div></blockquote><div><br></div></span><div>This is a good point and shows up the limitations of the current python-based type system.</div><div>Since we are working in a subset of python and are typechecking our code via mypy, </div><div>we cannot currently state or check sizes of types. </div><div><br></div><div>This brings up a question: should we introduce general refinement types?</div><div>E.g. poly1305_field = x:int{x >= 0 && x < 2**130 - 5}</div></div></div></blockquote><div><br></div></span><div>If it has to be true, we should have a way to express it?</div><div><br></div><div>Pre- and post- conditions?</div><span><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><div><div><br></div><div>Or at the very least, should we add length annotations a la rust?</div><div>E.g. chacha20_state = array[uint32; 16]</div><div><br></div>If we want to stay within Python, we would ned to hide such annotations within comments.</div><div>The benefit of sticking within Python syntax is that the code is immediately executable without any preprocessing.</div><div>However, if the syntax starts getting awkward, we should be open to adding a “light” erasure step that throws away some annotations.</div><div><span><br><blockquote type="cite"><div><div class="gmail_quote" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><div>Also, in the ctr.py example, is that assuming msg is some multiple of the block size?</div></div></div></blockquote><div><br></div></span><div>In counter_mode(), msg has an arbitrary size.</div><div>In block_encrypt() msg has size <= blocksize.</div><div><br></div><div>If msg < blocksize, then zip(keyblock,msg) truncates the result to the shorter length. </div><div>I realize this is confusing and undocumented, and I’ll try to rewrite this.</div></div></div></blockquote><div><br></div></span><div>Zipping with an explanation is fine.</div><div><div class="m_6809180135575754821m_6444996775725113078h5"><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><div><div><br></div><div><br></div><blockquote type="cite"><div><div class="gmail_quote" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><div>We're using LIONESS at work, which is only loosely specified, and we were thinking of writing a hacspec spec for it…</div></div></div></blockquote><div><br></div><div>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.</div><div><br></div><div>-Karthik</div><div><div class="m_6809180135575754821m_6444996775725113078m_560435129085547595h5"><br><blockquote type="cite"><div><div class="gmail_quote" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px"><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">I believe this syntax can be compiled to idiomatic Cryptol and F*, but we need to see how they translate to other formalisms.<br><br>As time goes along, we can add more constructs as needed, but let me informally describe the current features and the open questions:<br><br>INTEGERS:<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>The language includes arbitrary precision integers (int), and fixed-size integers (uint8, uint32, uint64, uint128; we can add more as needed.)<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>Standard arithmetic operators are overloaded over these integer types, and arithmetic overflows are treated with a wrapping semantics.<br>TUPLES (RECORDS?):<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>You can build and pass around tuples of values (Tuple[T1,…,Tn])<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>We have not included records yet, but we could, if desired, include JSON-like dictionaries (see the files in /test-vectors)<br>ARRAYS:<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>The only other data structures currently are arrays of fixed-length (array[T]).<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>You can read and write arrays, and you can read and write slices from arrays.<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>You can filter an array or apply a function to each element using array comprehensions (like in Python).<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>You can split an array into blocks and you can concatenate these blocks back into a flat array.<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>We are uncertain whether to include higher-order operators like map and reduce or to rely on comprehensions and for-loops instead<br>LOOPS:<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>The only looping construct is a for loop over a range.<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>If need be, we can add other looping constructs or recursion.<br>SIDE-EFFECTS (?):<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>Variables and arrays in the language can be modified, however we would like to limit all side-effects to local variables within functions.<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>Functions always return their outputs, they do not modify any of their arguments.<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>When arrays are passed into and out of functions, they are effectively copied in and copied out.<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>This part of the semantics needs some thinking and discussion to find a good middle-ground,<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>since the python syntax is naturally imperative, but most of the formal models we have looked<br> <span class="m_6809180135575754821m_6444996775725113078m_560435129085547595m_-1820130188764622080Apple-converted-space"> </span>at find it easier to reason about purely functional specificaion.<br><br>I am sure there is much else to look at and think about, but comments on the above would already be a good start.<br><br>Best regards,<br>Karthik<br><br><br><br><br><br>______________________________<wbr>_________________<br>Hacspec mailing list<br><a href="mailto:Hacspec@moderncrypto.org" target="_blank">Hacspec@moderncrypto.org</a><br><a href="https://moderncrypto.org/mailman/listinfo/hacspec" rel="noreferrer" target="_blank">https://moderncrypto.org/mailm<wbr>an/listinfo/hacspec</a></blockquote></div></div></blockquote></div></div></div><br></div></blockquote></div></div></div><br></div></div> <br>______________________________<wbr>_________________<br> Hacspec mailing list<br> <a href="mailto:Hacspec@moderncrypto.org" target="_blank">Hacspec@moderncrypto.org</a><br> <a href="https://moderncrypto.org/mailman/listinfo/hacspec" rel="noreferrer" target="_blank">https://moderncrypto.org/mailm<wbr>an/listinfo/hacspec</a><br> <br></blockquote></div><br></div> </div></div></blockquote></div></div></div><br></div></div> </blockquote></div><br></div></div>