Bug in name representation of Hax (Failure("invariant error"))

[geonnave]

When running cargo-hax ... into fstar I got a very long error message. Discussed with @W95Psp privately and he seems to have an idea on how to fix.

Code: this PR (commit 4a0a07c).

Command: cargo-hax -C -p edhoc-rs --no-default-features --features="crypto-hacspec, ead-none" \; into -i '-edhoc_rs::generate_connection_identifier_cbor -edhoc_rs::generate_connection_identifier' fstar

Output:

   Compiling edhoc-consts v0.1.0 (/home/gfedrech/Developer/inria/dev/edhoc-rs-FORK/consts)
   Compiling edhoc-crypto-trait v0.1.0 (/home/gfedrech/Developer/inria/dev/edhoc-rs-FORK/crypto/edhoc-crypto-trait)
   Compiling edhoc-ead-none v0.1.0 (/home/gfedrech/Developer/inria/dev/edhoc-rs-FORK/ead/edhoc-ead-none)
   Compiling edhoc-ead v0.1.0 (/home/gfedrech/Developer/inria/dev/edhoc-rs-FORK/ead)
   Compiling edhoc-crypto-hacspec v0.1.0 (/home/gfedrech/Developer/inria/dev/edhoc-rs-FORK/crypto/edhoc-crypto-hacspec)
   Compiling edhoc-crypto v0.1.0 (/home/gfedrech/Developer/inria/dev/edhoc-rs-FORK/crypto)
   Compiling edhoc-rs v0.2.1 (/home/gfedrech/Developer/inria/dev/edhoc-rs-FORK/lib)
Fatal error: exception Failure("invariant error")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Hax_engine__Concrete_ident.View.to_view in file "lib/concrete_ident/concrete_ident.ml", line 255, characters 21-57
Called from Hax_engine__Concrete_ident.MakeViewAPI.to_view in file "lib/concrete_ident/concrete_ident.ml", line 405, characters 43-62
Called from Hax_engine__Concrete_ident.MakeViewAPI.show in file "lib/concrete_ident/concrete_ident.ml", line 436, characters 4-13
Called from Hax_engine__Print_rust.Raw.pglobal_ident' in file "lib/print_rust.ml", line 94, characters 22-50
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 216, characters 8-15
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 299, characters 49-56
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Base__List.count_map in file "src/list.ml", line 479, characters 13-17
Called from Base__List.map in file "src/list.ml" (inlined), line 510, characters 15-31
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 215, characters 39-61
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 299, characters 49-56
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Base__List.count_map in file "src/list.ml", line 500, characters 13-17
Called from Base__List.map in file "src/list.ml" (inlined), line 510, characters 15-31
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 215, characters 39-61
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 272, characters 64-71
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 265, characters 10-19
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 265, characters 30-40
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 265, characters 30-40
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 265, characters 30-40
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.Raw.pexpr' in file "lib/print_rust.ml", line 265, characters 30-40
Called from Hax_engine__Print_rust.Raw.pexpr in file "lib/print_rust.ml", line 325, characters 12-20
Called from Hax_engine__Print_rust.pexpr_str in file "lib/print_rust.ml", line 586, characters 10-21
Called from Hax_engine__Ast_utils.Make.hax_failure_expr in file "lib/ast_utils.ml", line 632, characters 47-75
Called from Hax_engine__Phase_direct_and_mut.Make.Implem.ditem' in file "lib/phases/phase_direct_and_mut.ml", line 63, characters 6-510
Called from Hax_engine__Phase_direct_and_mut.Make.Implem.ditem_unwrapped in file "lib/phases/phase_direct_and_mut.ml", line 63, characters 6-510
Called from Hax_engine__Phase_direct_and_mut.Make.Implem.ditem in file "lib/phases/phase_direct_and_mut.ml", line 63, characters 6-510
Called from Base__List.concat_map.aux in file "src/list.ml", line 726, characters 34-40
Called from Hax_engine__Phase_utils.TracePhase.ditems.(fun) in file "lib/phase_utils.ml", line 201, characters 18-32
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Hax_engine__Phase_utils.BindPhase.ditems in file "lib/phase_utils.ml", line 224, characters 17-33
Called from Fstar_backend.apply_phases in file "backends/fstar/fstar_backend.ml", line 1157, characters 4-41
Called from Lib.run.run.(fun) in file "bin/lib.ml", line 72, characters 16-50
Called from Hax_engine__Diagnostics.Core.try_ in file "lib/diagnostics.ml", line 117, characters 26-32
Called from Lib.run in file "bin/lib.ml", line 85, characters 4-226
Called from Lib.main in file "bin/lib.ml", line 100, characters 11-24
Re-raised at Lib.main in file "bin/lib.ml", line 112, characters 6-42
Called from Dune__exe__Native_driver in file "bin/native_driver.ml", line 4, characters 8-70
error: hax-engine exited with non-zero code 2
       stdout: 
        stderr: 

error: could not compile `edhoc-rs` (lib) due to previous error

[geonnave]

Fixed in #364.