<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class=""><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; -webkit-text-stroke-width: 0px;"><div class="">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 class=""></div><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 class=""></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><br class=""></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 class=""></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><br class=""><blockquote type="cite" class=""><div class=""><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; -webkit-text-stroke-width: 0px;"><div class="">Also, in the ctr.py example, is that assuming msg is some multiple of the block size?</div></div></div></blockquote><div><br class=""></div><div>In counter_mode(), msg has an arbitrary size.</div><div>In block_encrypt() msg has size <= blocksize.</div><div><br class=""></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><br class=""></div><div><br class=""></div><blockquote type="cite" class=""><div class=""><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; -webkit-text-stroke-width: 0px;"><div class="">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 class=""></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 class=""></div><div>-Karthik</div><br class=""><blockquote type="cite" class=""><div class=""><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; -webkit-text-stroke-width: 0px;"><div class=""><br class=""></div><div class=""> </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 class=""><br class="">As time goes along, we can add more constructs as needed, but let me informally describe the current features and the open questions:<br class=""><br class="">INTEGERS:<br class=""> <span class="Apple-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 class=""> <span class="Apple-converted-space"> </span>Standard arithmetic operators are overloaded over these integer types, and arithmetic overflows are treated with a wrapping semantics.<br class="">TUPLES (RECORDS?):<br class=""> <span class="Apple-converted-space"> </span>You can build and pass around tuples of values (Tuple[T1,…,Tn])<br class=""> <span class="Apple-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 class="">ARRAYS:<br class=""> <span class="Apple-converted-space"> </span>The only other data structures currently are arrays of fixed-length (array[T]).<br class=""> <span class="Apple-converted-space"> </span>You can read and write arrays, and you can read and write slices from arrays.<br class=""> <span class="Apple-converted-space"> </span>You can filter an array or apply a function to each element using array comprehensions (like in Python).<br class=""> <span class="Apple-converted-space"> </span>You can split an array into blocks and you can concatenate these blocks back into a flat array.<br class=""> <span class="Apple-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 class="">LOOPS:<br class=""> <span class="Apple-converted-space"> </span>The only looping construct is a for loop over a range.<br class=""> <span class="Apple-converted-space"> </span>If need be, we can add other looping constructs or recursion.<br class="">SIDE-EFFECTS (?):<br class=""> <span class="Apple-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 class=""> <span class="Apple-converted-space"> </span>Functions always return their outputs, they do not modify any of their arguments.<br class=""> <span class="Apple-converted-space"> </span>When arrays are passed into and out of functions, they are effectively copied in and copied out.<br class=""> <span class="Apple-converted-space"> </span>This part of the semantics needs some thinking and discussion to find a good middle-ground,<br class=""> <span class="Apple-converted-space"> </span>since the python syntax is naturally imperative, but most of the formal models we have looked<br class=""> <span class="Apple-converted-space"> </span>at find it easier to reason about purely functional specificaion.<br class=""><br class="">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 class=""><br class="">Best regards,<br class="">Karthik<br class=""><br class=""><br class=""><br class=""><br class=""><br class="">______________________________<wbr class="">_________________<br class="">Hacspec mailing list<br class=""><a href="mailto:Hacspec@moderncrypto.org" class="">Hacspec@moderncrypto.org</a><br class=""><a href="https://moderncrypto.org/mailman/listinfo/hacspec" rel="noreferrer" target="_blank" class="">https://moderncrypto.org/<wbr class="">mailman/listinfo/hacspec</a></blockquote></div></div></blockquote></div><br class=""></body></html>