Bug: ill-typed projection element

[msprotz]

In Eurydice, I am traversing the Charon representation of the following function: https://github.com/cryspen/libcrux/blob/franziskus/mldsa-c-ci/libcrux-ml-dsa/src/simd/avx2.rs#L140-L142

To observe this, run ./boring.sh in the libcrux-ml-dsa subdirectory, on an x64 machine (this code is disabled on arm64).

This is the representation:

Visiting function: libcrux_ml_dsa::simd::avx2::{(libcrux_ml_dsa::simd::traits::Operations for libcrux_ml_dsa::simd::avx2::vector_type::AVX2SIMDUnit)}::ntt::closure
  fn libcrux_ml_dsa::simd::avx2::{libcrux_ml_dsa::simd::traits::Operations for libcrux_ml_dsa::simd::avx2::vector_type::AVX2SIMDUnit}::ntt::closure<0, 1>(state^1 : &0 mut ((&1 (@Array<core::core_arch::x86::__m256i, 32: usize>))), i^2 : usize) -> libcrux_ml_dsa::simd::avx2::v
ector_type::AVX2SIMDUnit
{
    v@0 : libcrux_ml_dsa::simd::avx2::vector_type::AVX2SIMDUnit;
    state^1 : &0 mut ((&1 (@Array<core::core_arch::x86::__m256i, 32: usize>)));
    i^2 : usize;
    v@3 : core::core_arch::x86::__m256i;
    v@4 : usize;
    v@5 : &'_ (@Array<core::core_arch::x86::__m256i, 32: usize>);
    v@6 : &'_ (core::core_arch::x86::__m256i);

    v@4 := copy i^2;
    v@5 := &*((*(state^1)).0);
    v@6 := move @ArrayIndexShared<'_, core::core_arch::x86::__m256i, 32: usize>(move v@5, copy v@4);
    v@3 := copy *(v@6);
    v@0 := libcrux_ml_dsa::simd::avx2::vector_type::AVX2SIMDUnit { coefficients = move v@3; };
    drop v@4;
    drop v@3;
    return
  }

When I translate v@5 := &*((*(state^1)).0);, I call expression_of_place which prints out both the sub-place and the path element, at this location: https://github.com/AeneasVerif/eurydice/blob/main/lib/AstOfLlbc.ml#L557 using the following debug printing (in my local copy):

      L.log "AstOfLlbc" "sub_place=%s\npe=%s\n" (C.show_place sub_place) (C.show_projection_elem pe);

My understanding is that the sub-place, e.g., has type "tuple", and the path element is valid for that type, e.g. .0 or .1.

However, this is the debug output that I get:

sub_place={ Generated_Expressions.kind =
  (Generated_Expressions.PlaceProjection (
     { Generated_Expressions.kind = (Generated_Expressions.PlaceBase 1);
       ty =
       (Generated_Types.TRef (Generated_Types.RErased,
          (Generated_Types.TArrow
             { Generated_Types.binder_regions = [];
               binder_value =
               ([(Generated_Types.TLiteral
                    (Generated_Values.TInteger Generated_Values.Usize))
                  ],
                (Generated_Types.TAdt ((Generated_Types.TAdtId 18),
                   { Generated_Types.regions = []; types = [];
                     const_generics = []; trait_refs = [] }
                   )))
               }),
          Generated_Types.RMut))
       },
     Generated_Expressions.Deref));
  ty =
  (Generated_Types.TArrow
     { Generated_Types.binder_regions = [];
       binder_value =
       ([(Generated_Types.TLiteral
            (Generated_Values.TInteger Generated_Values.Usize))
          ],
        (Generated_Types.TAdt ((Generated_Types.TAdtId 18),
           { Generated_Types.regions = []; types = []; const_generics = [];
             trait_refs = [] }
           )))
       })
  }
pe=(Generated_Expressions.Field ((Generated_Expressions.ProjTuple 1), 0))

My question is: why does it make sense to project field element 0 out of something that has an arrow type?

Note that I am only recursing on sub-places constructed by charon, so I don't think I'm rebuilding incorrect type information anywhere.

[Nadrieril]

My question is: why does it make sense to project field element 0 out of something that has an arrow type?

Indeed that makes no sense. The truth is that this is not an arrow type, this is a closure type, but we've been pretending the two are the same for a while. This is part of #194.