hacspec / hacspec Goto Github PK

It is currently not allowed to use let x = if ... bindings. But it is also not allowed to use let declarations let x: u8;.
This leads to Rust compiler warnings because code like the following is necessary where the first assignment of x is clearly unnecessary.

let mut x = 0u8;
if y > 5 {
    x = 1;
} else {
    x = 2;
}

hacspecs currently don't have a way for error handling. I currently see two things we need.

• option types/results for returning errors (we currently return tuples of the form (bool, T) right now, which isn't very nice)
• allow to stop execution early. There are two parts to this, one is more needed than the other.
  • allow to breaking out of loops
  • allow to return early (from inside an if statement)

Hello, I am wondering if it is possible to have the hacspec compiler also target Coq in addition to F*? The languages are very similar, so I am hoping that (at least the translation) would be fairly straightforward, given the existing code for translating to F*.
I would be interested in making these contributions, although I am not a Rust expert.
Could you help me getting started? So far I have simply made a file rustspec_to_coq.rs, similar to rustspec_to_fstar.rs, but I don't know how to integrate it into the rest of the codebase, in particular how to test it.

Very much appreciated!

I had the typechecker set up and running successfully yesterday. But, when I opened it today and ran cargo hacspec hacspec-aes-ccm or cargo +nightly-2021-06-15 hacspec hacspec-aes-ccm it gave the below error.

I got the same error while running cargo hacspec hacspec-gimli as well. Between the successful and failed runs of the typechecker, the only thing I did was run cargo test on aes-ccm. I'm not sure if that is the cause of this or whether it is something else. Any idea how I can fix this?

The link to the original paper on hacspec "https://www.franziskuskiefer.de/publications/hacspec18/" does not contain the paper.

Use verified BigInts from HACL*.

Add an option to allow using hacspec with no_std.

I can see why you would need that for performance improvements, but there should be a comment saying that this is equivalent to the identity function semantics-wise because the formal model of hacspec does not know that its Seqs are resizable arrays.

Originally posted by @denismerigoux in #130 (comment)

I'm trying to run the typechecker and it is giving me this error. "error: a bin target must be available for cargo run". This is de command I'm running on my machine:
"$cargo run --
-L ~/Documents/Universidade/TESE/projects/hacspec_test/spec_test/target/debug/deps
--crate-type=lib --edition=2018
--extern=hacspec-lib
-Zno-codegen
~/Documents/Universidade/TESE/projects/hacspec_test/spec_test/src/main.rs "

Because the typechecker currently expects a block in the else branch else if can't be used.

error[Hacspec]: block of statements expected in the else branch in Hacspec

Implement support for enums in hacspec.

enum HashAlgorithm {
    SHA256,
    SHA384,
}

Supported operations

• match
• if let

1. when defining an abbreviation for a tuple type, the typechecker sometimes expands the tuple and tries to match it with the type name, failing with errors like the one below (where PolyState is an abbreviation for (FieldElement, FieldElement, PolyKey):

  --> /Users/bhargava/Desktop/repositories/hacspec/examples/chacha20poly1305/src/chacha20poly1305.rs:21:41
   |
21 |         st = poly1305_update1(16,&block,st); // This is the only line that changes from poly1305_update.
   |                                         ^^```

So this creates a Seq of size 0 doesn't it? Why do you need that in hacspec, since pushing elements to a Seq is forbidden ?

Originally posted by @denismerigoux in #130 (comment)

For generating F* code that typechecks out of the box, we need to add some range annotations to source hacspec.

I suggest we add a macro which is something like:
range!(<new type name>, <some numeric type>, start, end)

This gets translated to the F* refinement type:
type <new type name> = x:<some numeric type>{x >= start /\ x < end}

In practice, just supporting the above for usize would already solve most of the problems in our current specs.

I'm one of the leads of the RustCrypto project. I just opened an issue about trying to do some sort of hacspec integration:

RustCrypto/meta#9

One possibility I suggested was using Project Oak's Rust Verification Tools (RVT) to prove equivalence between RustCrypto implementations and the hacspec reference implementations. RVT provides a sort of abstract harness with a common API for either equivalence proving with symbolic execution (using KLEE), or property-based testing using proptest (which would simplify testing in resource-constrained CI environments). See the Rust testing or verifying: Why not both? blog post for more information on RVT.

I mainly opened this issue to give you a heads up that we're interested in this sort of thing, but we'd also love to encourage people to help work on this as it seems like an interesting use case for hacspec.

We recently ran into the issue where we had

sha256.rs

array!(Digest, 16);

lib.rs

use sha256::*;

type Digest ByteSeq;

fn foo() {
    let d = Digest::new(5);
}

In this case the Digest name clashes. This is fine for rustc but the hacspec typechecker fails when calling new because it thinks it's the array, where new doesn't require any arguments.
This creates very hard to track down typechecker errors.

hir_to_rustspec.rs should check names when importing them.

#134 introduces the macros byte_seq! and public_byte_seq! to create byte sequences from Rust arrays in the same way as is possible for arrays already. The macros have to be added to the typechecker and the backends.

Originally posted by @denismerigoux in #134 (comment)

Only secret_array is allowed right now.
This also implies that only array! has to be used instead of bytes! right now.

Currently array!(State, 8, U8, type_for_indexes: StateIdx) is a different implementation than bytes!(State, 8). That's confusing and unnecessary.

Implement a spec for BIP32-Ristretto

see also iqlusioninc/crates#738

Context

One can use cargo install to install in the user's path (on Linux in ~/.cargo/bin) binaries implemented by a Rust crate. It would be nice for hacspec to be distributed that way, as it would be well-integrated with the Rust ecosystem.

Another hook we want to use is the third-party cargo subcommand system : https://github.com/rust-lang/cargo/wiki/Third-party-cargo-subcommands.

Goal

Basically, we want to be able to run cargo hacspec from inside a spec's folder, and this would launch typechecking on the spec's crate.

We could imagine using something cargo hacspec -- -o Foo.fst for compiling the current crate into an F* file.

Current issues

Currently, you can cargo install hacspec but then it complains about not being able to find dynamically shared libraries :

~/.cargo/bin/cargo-hacspec: error while loading shared libraries: librustc_driver-397eb455b7db4ba5.so: cannot open shared object file: No such file or directory

The issue seems to reside in setting the correct search path for Rust-related dynamic libraries. These libraries are stored inside a folder caleed sysroot in the Rust ecosystem. The sysroot can apparently be found using rustc --print sysroot. Other environment variables problems are likely to arise. Especially, currently hacspec is called with an -L option pointing to the folder where all the .rlib files for the current crate's dependencies are stored. It would be nice if we could omit this option, maybe via cargo setting an environment variable.

For inspiration, one can look at how Clippy is solving these problems : https://github.com/rust-lang/rust-clippy/blob/master/src/main.rs. It's expected that the modifications will concern only language/src/{main.rs, cli.yml} :)

I created tons of random tests for the gimli aead function, same as I had done for the gimli hash (#110). Turns out, both the encryption and decryption algorithms have the exact same error, and is also similar to the one in the hash function.

The bug is that when the plaintext to encrypt or the ciphertext to decrypt have a multiple of 16 number of bytes, the program crashes while processing it and doesn't even give an output. This occurs when dividing the message into blocks of 16 bytes, the last block of 0 bytes isn't considered by num_chunks. Thus, an index out of bounds error comes up when the program finds the last block to be of 16 byte length instead of 0.

There are 2 different fixes to this issue that I've tested and which seemed to fix the bug:

1. We can do away with the use of num_chunks and instead just do: let num_chunks = message.len() / rate + 1;.
2. We could add an if condition in order to do one more iteration when the number of bytes is a multiple of 16, like it was done here: 9c79ec6.

This fix would need to be added to both process_msg and process_ct functions in gimli.rs. For the gimli hash, we had taken processing of the last non-full block of the text outside of the loop by using num_exact_chunks. However, unlike that case, both the non-full and complete blocks share some of the operations so, if we took the non-full block out of the loop we would end up duplicating the same code, which feels unnecessary.

Please let me know which of the 2 fixes should be implemented or whether there is an alternative fix that I haven't thought of, and I'd be happy to make the changes in a PR. Thanks!

Clicking on any link under Examples section results in 404 error.

Hi!
In the Language.md and also in Arithmetic.md I see that it has the poly!() function but I'm not quite getting how to use it.
I didn't find any example that uses it.
For context, I'm asking because I'm trying to do an poly1305 implementation in hacspec, that has fewer lines of code than the example provided.

To make unit testing easier the typechecker should ignore #[cfg(test)] parts of hacspecs.

Thanks to @franziskuskiefer for spotting. This is allowed

let x = other()?;

but this isn’t?

x = other()?; // where x is mut

Remove support for arrays without index type.

I am currently trying to extract tests (e.g. QuickCheck tests) through hacspec to proof assistants (Coq) such that the tests can be verified / used in these proof environments.

Current issues are that tests are not required to be written in hacspec, which then fails when trying to create terms for the proof assistant.

In addition the chunk processing with get_chunk the library should support something like get_exact_chunk that only returns full chunks and a get_remainder to get the last, non-full chunk.

The problem is that from_canvas just forces the value into the scalar. Instead we have to check that the value is in [1, order-1] and return an error if not. We could do this in the P256 code. But it's a pretty common functionality such that I think it would make sense to have it in the library.

Originally posted by @franziskuskiefer in #134 (comment)

nat_mod should check that scalars are valid instead taking the remainder

It is currently impossible to downcast integers, e.g. usize to u8, which is needed sometimes.
It would probably be best to allow TryFrom conversions that have to be unwrapped, e.g. u8::try_from(x).unwrap() or provide a library function wrapping this.

From the Rust guide:

struct Struct;

impl Struct {
    const ID: u32 = 0;
}

fn main() {
    println!("the ID of Struct is: {}", Struct::ID);
}

In #126 bitwise operators for sequences were introduced but the typechecker doesn't know about them yet.
In order to use them in #139 the typechecker needs to get updated.

Currently I am working on an additional option for aes.rs (a 256bit aes version)

Related to #55

I think it'd be interesting to be able to annotate functions written in the hacspec subset of Rust in such a way that they could be extracted out of a larger Rust program and treated as hacspec.

As a concrete example, here is an SBox implementation from the RustCrypto aes crate written in such a subset:

https://github.com/RustCrypto/block-ciphers/blob/master/aes/src/soft/fixslice32.rs#L780-L954

(note there are many other functions in the same module which fit this basic profile)

Concretely what I'm thinking of is something like adding an annotation such as:

#[hacspec]
fn hacspec_compatible_function(...) {
   [...]
}

There are a number of different ways you could potentially use such an annotation.

One would be writing a preprocessor that parses each module with syn, looks for code annotated with #[hacspec] and retains it, and removes everything else.

It looks like the typechecker doesn't handle loop ranges well
The following snipets will fail to typecheck.

// This will fail with "loop range bound should be an integer but has type u32"
for i in 0u32..7u32 {}

type MyIntegerType = u32;
// This will fail with "loop range bound should be an integer but has type MyIntegerType"
for i in 0u32..MyIntegerType {}

type MyIntegerType = u32;
// This will fail with "this expression of type MyIntegerType cannot be casted"
for i in 0..(MyIntegerType as usize) {}

This makes it impossible to use type aliases for loops.

The typechecker rejects hacspecs for inline blocks even if there's not actually a block.

error[Hacspec]: inline blocks are not allowed in Hacspec
   --> /home/franziskus/repos/hacspec/protocols/tls_cryptolib/src/lib.rs:349:40
    |
349 |           SignatureResult::Ok((r, s)) => {
    |  ________________________________________^
350 | |             // The ASN.1 encoding happens later on the outside.
351 | |             concat_signature(r, s)
352 | |         }

So technically this is a block because of the {} but the braces are only added because of the comment. This should be allowed. If it's too much trouble to allow this we need a good description of how to handle a case like this.

cc @denismerigoux

Using a constant from a different crate causes error[Hacspec]: original id not found in name context.

There are some primitives in the hacspec python version we could re-implement here

• XMSS
• VRF
• RSA-PSS
• Kyber
• Elligator2
• Curve448

There are some problems with poly.inv().
The following Code snippet displays the problem if you run it with "use hacspec::prelude::*;" in scope

fn inv_problem(){
    // define Ring with highest deg 11, and modulo 32, no difference between i128 and u128
    poly!(ZxN, u128,11,32,&[(0,31),(11,1)]);

   
    let f = ZxN::new(&[(0,31),(1,1),(2,1),(4,31),(6,1),(9,1),(10,31)]);
    let f_inv = ZxN::new(&[(0,5),(1,9),(2,6),(3,16),(4,4),(5,15),(6,16),(7,22),(8,20),(9,18),(10,30)]);
    // expected value f * f_inv = [(0,1),(1,0),..,(11,0)]
    println!("f * f_inv = {:?}",f.mul(f_inv));
    // but here occurs an Err 
    assert_eq!(f.inv(),f_inv);
}

Similarly to #97 it would be great to have an attribute like #[unsafe_hacspec] that can be added to functions in hacspec that

• have a signature that's in hacspec
• have a body that's not in hacspec

This would allow for integration of hacspec code into other Rust code. These functions can be used to convert between Rust and hacspec types and call into other Rust code.

Using a custom

[lib]
path = "src/gimli.rs"

sometimes crashes the typechecker (depending on the file name).

thread 'rustc' panicked at 'called `Option::unwrap()` on a `None` value', compiler/rustc_metadata/src/rmeta/decoder.rs:1514:47

The crash is caused by this call

To reproduce just create an empty crate with a lib as described above and run the typechecker on it.

@denismerigoux any idea what's causing this?

The hacspec-lib contains functions that are nor in hacspec (marked with the not_hacspec attribute). These functions are not allowed in hacspec but can be used right now. There are two options
i) remove not_hacspec functions from the library to hacspec-dev
ii) fail in the typechecker on not_hacspec functions

The following should be allowed by the typechecker

for _ in 0..5 { }

Originally posted by @denismerigoux in #134 (comment)

Add SPARKLE spec

https://csrc.nist.gov/CSRC/media/Projects/lightweight-cryptography/documents/round-2/spec-doc-rnd2/sparkle-spec-round2.pdf

Right now the P256 spec doesn't do any sort of input validation.

• add point validation
• add scalar validation (#137)

The library has grown a lot and contains a lot of unnecessary functionality and complexity.
This issue tracks cleaning it up.

It also has to be decided what to put into the library and what should be separate libraries that can be pulled in only when needed.

Related issues

• #226

External consumers

• https://github.com/AU-COBRA/AUCurves/tree/main/src/Hacspec

Tracking NTRU Prime hacspec implementation by @TomerHawk.