Skip to content

Feature request #1

Jump to bottom
bacelar edited this page Dec 13, 2021 · 2 revisions

Parametrised imports in Jasmin

Goal

To make it possible to instantiate a module's parameter when importing in a Jasmin program. The direct motivation for it is a simple library for bignum operations, which is parametrised by their size (numbers of limbs). Currently, the require command performs a pure syntactical inclusion of the requested file -- hence, we have defined the parameter prior to the inclusion, such as in

param int NLIMBS=7;
require "bn_generic.jinc"

But such a workaround has several drawbacks:

  • The included file is not a proper "compilation unit" for Jasmin (it lacks the uninstantiated param int NLIMBS declaration). From the code generation perspective, this is not really an issue (we need fully instantiated programs to generate code), but is certainly relevant for extraction into EC since we would like to preserve the module's genericity.
  • It would not allow to perform multiple instantiations of the parametric module. This is arguably a less common scenario, but worth to look at when designing the feature.

A closely related feature is a namespace mechanism for Jasmin -- the current proposal shall be adjusted/merged with such a mechanism.

Overall, this feature request affects the Jasmin loader and the extraction mechanism into EC. It appears to have no (or little) impact on the certified part of the compiler.

Feature proposal

We split the parameterised import mechanism in different elementary features.

Qualified require clause

require "module.jinc" as mmm

After the inclusion, non-exported declarations from module.jinc would be accessible with prefix mmm.. Moreover, upon extraction into EC, the qualified accesses should preserve the indirection (e.g. to mmm.M.f, from a theory mmm presumably cloned from the theory extracted from module.jinc).

The qualified import could also be used to allow a fully backward compatible solution wrt the current require clause (that performs textual inclusion) -- both the modularised extraction and the remaining instantiation features described bellow could be allowed/triggered by the qualified variant.

Instantiation of int parameters

An example:

require "bn_generic.jinc" as bn where NLIMBS = 7

And possibly also:

require "bn_generic.jinc" as bn2 where NLIMBS = 14

ISSUE: it does not seems to make sense to qualify exported declarations, but that would preclude multiple instantiations in the presence of exported declarations. It does not seems to be critical, as we can always do the exported declarations later, but one can also adopt some sort of name-mangling to translate the exported definitions (e.g. use the prefix bn_ instead of bn. for exported functions...).

Non-int parameters

In Jasmin parameters are restricted to inline ints. But it seems to make sense to generalise those to other datatypes, that would be instantiable with global variables. Again, the direct motivation is the library of bignums, where some functions assume the existence of some global variables such as the prime used in modular operations. It is conceivable that Jasmin could accept parameters such as:

param int NLIMBS;
param u64[NLIMBS] P;

And then allow the import

u64[7] glob_p = { ... };
require "bn_generic_modular.jinc" as bn where NLIMBS = 7, P = glob_p

Again, upon extraction to EC, these would be operators that would be instantiated to concrete values during cloning.

Procedural parameters

What seems to be a natural extension to the previous features is to allow also procedures (Jasmin functions) to act as parameter of modules. For example, we could think of a module for the HMAC construction to be parametric on the hash function operations.

param int HASHCTXT;
param int HASHLEN;
param fn hash_init(reg ptr u64[HASHCTXT] ctxt) -> reg ptr u64[HASHCTXTSIZE];
param fn hash_update(reg ptr u64[HASHCTXT] ctxt, reg u64 inbuf size) -> reg ptr ctxt;
param fn hash_finish(reg ptr u64[HASHCTXT] ctxt, reg ptr u64[HASHLEN]) -> reg ptr u64[HASHCTXT], reg ptr u64[HASHLEN];

Again, during import, these parameters could be instantiated

require "sha3.jazz" as sha3
require "hmac.jinc" as hmac_sha3 where HASLEN = 256, ....., hash_finish = sha3.finish

But such an extension appears to have a bigger impact on the extraction into EC: module's code should be extracted into EC in a parametrised module (whose module type collects signatures for the procedural parameters). During instantiation, a module should be created 'on-the-fly' to be passed to the parametric module (it should be reasonable to enforce fully instantiation of the procedural parameters, otherwise one should deal with yet another parametric module...). In the end, the increased complexity seems an invitation to consider this feature only after implementing the other ones!

Clone this wiki locally