Bug: architecture-specific behavior

[msprotz]

First OSX device, setup is as follows:

jonathan@absinthe:~/Code/eurydice (protz/preserve_const) $ uname -a
Darwin absinthe 24.6.0 Darwin Kernel Version 24.6.0: Mon Jul 14 11:28:17 PDT 2025; root:xnu-11417.140.69~1/RELEASE_X86_64 x86_64
jonathan@absinthe:~/Code/eurydice (protz/preserve_const) $ charon version
0.1.123
jonathan@absinthe:~/Code/eurydice (protz/preserve_const) $ (cd ../charon && git rev-parse head)
dde1bc4fe5a8cf7b15051411ec6a6e46409117a7

If I run make -B test/fn_higher_order.llbc && charon pretty-print test/fn_higher_order.llbc, then I see an opaque function here:

// Full name: fn_higher_order::more_sum_lst
fn more_sum_lst<'_0>(@1: &'_0 (Array<i32, 3 : usize>)) -> i32

(nothing follows)

and I get the following Charon errors:

thread 'rustc' panicked at compiler/rustc_middle/src/ty/context.rs:2946:9:
assertion failed: eps.array_windows().all(|[a, b]|
        a.skip_binder().stable_cmp(self, &b.skip_binder()) !=
            Ordering::Greater)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
warning: Hax panicked when translating `core::iter::traits::collect::IntoIterator`.
 --> /rustc/library/core/src/iter/traits/collect.rs:282:1


thread 'rustc' panicked at compiler/rustc_middle/src/ty/context.rs:2946:9:
assertion failed: eps.array_windows().all(|[a, b]|
        a.skip_binder().stable_cmp(self, &b.skip_binder()) !=
            Ordering::Greater)
warning: Hax panicked when translating `core::iter::traits::collect::IntoIterator`.
 --> /rustc/library/core/src/iter/traits/collect.rs:282:1

warning: function `empty_ptr` is never used
  --> test/fn_higher_order.rs:14:4
   |
14 | fn empty_ptr(f : fn() -> i32) -> i32 {
   |    ^^^^^^^^^
   |
   = note: `#[warn(dead_code)]` on by default

warning: function `unit_empty_ptr` is never used
  --> test/fn_higher_order.rs:18:4
   |
18 | fn unit_empty_ptr(f : fn()) {
   |    ^^^^^^^^^^^^^^

warning: 2 warnings emitted

Second OSX device, setup is as follows:

jonathan@verveine:~/Code/eurydice (protz/preserve_const) $ uname -a
Darwin verveine 24.6.0 Darwin Kernel Version 24.6.0: Mon Jul 14 11:30:55 PDT 2025; root:xnu-11417.140.69~1/RELEASE_ARM64_T6031 arm64
jonathan@verveine:~/Code/eurydice (protz/preserve_const) $ charon version
0.1.123
jonathan@verveine:~/Code/eurydice (protz/preserve_const) $ (cd ../charon && git rev-parse head)
dde1bc4fe5a8cf7b15051411ec6a6e46409117a7

If I run the same command, then I see a function body here:

/ Full name: fn_higher_order::more_sum_lst
fn more_sum_lst<'_0>(@1: &'_0 (Array<i32, 3 : usize>)) -> i32
{
    let @0: i32; // return
...

and the following Charon errors:

warning[E9999]: Could not find a clause for `Binder { value: <A as std::iter::IntoIterator>, bound_vars: [] }` in the current context: `Ambiguity`
   --> /Users/jonathan/.rustup/toolchains/nightly-2025-07-08-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/range.rs:845:1
    |
845 | impl<A: Step> Iterator for ops::Range<A> {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!

warning: function `empty_ptr` is never used
  --> test/fn_higher_order.rs:14:4
   |
14 | fn empty_ptr(f : fn() -> i32) -> i32 {
   |    ^^^^^^^^^
   |
   = note: `#[warn(dead_code)]` on by default

warning: function `unit_empty_ptr` is never used
  --> test/fn_higher_order.rs:18:4
   |
18 | fn unit_empty_ptr(f : fn()) {
   |    ^^^^^^^^^^^^^^

warning: 3 warnings emitted

Amusingly, the Charon run that exhibits three warnings on Arm64 seems to produce better results than the Charon run on x86_64 that only exhibits two warnings.

[Nadrieril]

What options are you passing to charon? Also could you paste the code of more_sum_lst?

The most obvious explanation is that this code invoques platform-specific code and that the different architectures trigger differnt charon bugs. In other words ideally I'd like a reproducer for the core bug. I've seen this array_windows business somewhere but I forgot where.

[msprotz]

jonathan@absinthe:~/Code/eurydice (protz/preserve_const) $ make -Bn test/fn_higher_order.llbc
# --mir elaborated --add-drop-bounds
/Users/jonathan/Code/charon/bin/charon rustc --preset=eurydice --dest-file "test/fn_higher_order.llbc"  -- test/fn_higher_order.rs

(sorry in a rush)

[ssyram]

The sorting problem relates to #790 and should be resolved by AeneasVerif/hax#2.