Makefile error: Identifier not found: [Core.Iter.Traits.Iterator.f_position]

[elenaf9]

Thank you for your great work on this Project!

We ran into an error due to some missing identifier. We are using Iterator::position in our code. Error is

* Error 72 at Riot_rs_runqueue.Runqueue.Clist.fst(83,40-83,50):
  - Identifier not found: [Core.Iter.Traits.Iterator.f_position]
  - Module Core.Iter.Traits.Iterator resolved into Core.Iter.Traits.Iterator,
    definition f_position not found

1 error was reported (see above)
make[1]: *** [Makefile:86: .cache/Riot_rs_runqueue.Runqueue.Clist.fst.checked] Error 1
make[1]: Leaving directory '/home/runner/work/RIOT-rs/RIOT-rs/src/riot-rs-runqueue/proofs/fstar/extraction'
make: *** [Makefile:48: all] Error 2

See https://github.com/future-proof-iot/RIOT-rs/actions/runs/8662006305/job/23753096732?pr=248.

Can this be fixed somehow on your side or do we have to change our code?

[elenaf9]

Friendly ping. Any pointers that you could give me on how to fix this?

We ran in the Identifier not found Error again for another type: https://github.com/elenaf9/RIOT-rs/actions/runs/8969984735/job/24632495409.

[franziskuskiefer]

This looks like some missing piece in the core library model. A small reproducer is

pub fn position() {
    let idxs = [1, 2, 3, 4];
    let prev = idxs.iter().position(|next_idx| *next_idx == 5).unwrap();
}

This generates

let position (_: Prims.unit) : Prims.unit =
  let idxs:t_Array i32 (sz 4) =
    let list = [1l; 2l; 3l; 4l] in
    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 4);
    Rust_primitives.Hax.array_of_list 4 list
  in
  let _, out:(Core.Slice.Iter.t_Iter i32 & Core.Option.t_Option usize) =
    Core.Iter.Traits.Iterator.f_position (Core.Slice.impl__iter (Rust_primitives.unsize idxs
            <:
            t_Slice i32)
        <:
        Core.Slice.Iter.t_Iter i32)
      (fun next_idx ->
          let next_idx:i32 = next_idx in
          next_idx =. 5l <: bool)
  in
  let prev:usize = Core.Option.impl__unwrap out in
  ()

Core.Iter.Traits.Iterator.f_position is currently not defined here https://github.com/hacspec/hax/blob/main/proof-libs/fstar/core/Core.Iter.Traits.Iterator.fst

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[elenaf9]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

This is still relevant for us.

[franziskuskiefer]

@W95Psp @cmester0 Let's put this on the list of core library functions to get done.

[W95Psp]

Sorry for the late reply. Adding this operator is complicated because of the current implementation of the core library in F*. @cmester0 is working toward a new design for the library, which should hopefully help with this issue.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.