fstar generation fails with Unimplemented on array! macro

[geonnave]

Output when building (using docker):

• edhoc-rs main branch (commit d3629bb8c456691aa4fee4330e7447b4aedac402)

bash-5.2# cargo-circus into fstar                                                                                      
   Compiling edhoc-consts v0.1.0 (/edhoc-rs/consts)                                                                    
error[CE0001]: Diagnostics.Context.ThirImport: Unimplemented { issue_id: None, details: Some("Repeat") }               
  --> consts/src/lib.rs:45:26                                                                                          
   |                                                                                                                   
45 |                 content: [0u8; MAX_MESSAGE_SIZE_LEN],                                                             
   |                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^                                                              
                                                                                                                       
error: could not compile `edhoc-consts` due to previous error                                                          

• older version of edhoc-rs, before some major changes (commit b74a265661d3987c26c79b51641f246b5fa26c5c)

bash-5.2# cargo-circus into fstar 
   Compiling edhoc-consts v0.1.0 (/edhoc-rs/consts)
error[CE0001]: Diagnostics.Context.ThirImport: Unimplemented { issue_id: None, details: Some("Repeat") }
   --> consts/src/lib.rs:123:5
    |
123 |     array!(BytesEad2, 0, U8);
    |     ^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: this error originates in the macro `_array_base` which comes from the expansion of the macro `array` (in Nightly builds, run with -Z macro-backtrace for more info)

error: could not compile `edhoc-consts` due to previous error

How to reproduce

Basically, clone edhoc-rs, checkout the appropriate branch/commit, remove default-features = false from edhoc-rs/hacspec/Cargo.toml, and run cargo-circus into fstar.

Here is a quick copy-paste using docker:

git clone [email protected]:hacspec/hacspec-v2.git && cd hacspec-v2
docker build -f .docker/Dockerfile . -t hacspec-v2

cd ..
git clone [email protected]:openwsn-berkeley/edhoc-rs.git && cd edhoc-rs
sed -i -E "s/(edhoc-crypto.*), default-features = false(.*)/\1\2/" ./hacspec/Cargo.toml
docker run --rm -v $(pwd):/edhoc-rs hacspec-v2 bash -c "cd edhoc-rs/hacspec && cargo-circus into fstar"

[franziskuskiefer]

This should get fixed in #98.

[W95Psp]

I tried just now with @98 merged, I'm able to translate the crate edhoc-consts, but then, I hit #27.
I think this issue should be closed, but you hit another bug right after :(

[geonnave]

Thanks for fixing this. As per #27, no problem, I added a note there so we can close this and still keep track of the whole context.