Fix Failure("nth") crash in remove_unused_parameters

[elefthei]

Fixes #677

Problem

remove_unused_parameters in lib/Simplify.ml crashes with Failure("nth") when bundling modules where a function call site has more actual arguments than the callee's formal type parameters (as reported by flatten_arrow).

This happens when erased/ghost parameters are passed as () at call sites, but the callee's type signature doesn't include them (e.g., external functions like Pulse.Lib.Array.PtsTo.op_Array_Access whose ghost args were erased from the type but not from call sites).

Root Cause

In unused_i (line 236), List.nth ts i = TUnit is called without bounds checking. The update_table_current call at line 344 in visit_EApp iterates over actual arguments es and calls unused arg_i for each — but arg_i can exceed List.length ts when there are more actual args than formal type params. The length guard at line 353 correctly handles this for the main transformation path, but update_table_current is invoked before that guard.

Fix

Add a bounds check so unused_i returns false for out-of-bounds indices (conservative: don't eliminate unknown params):

-    List.nth ts i = TUnit
+    i < List.length ts && List.nth ts i = TUnit

Reproduction

Extract a Pulse module with .fsti interface (making implementations private), create a wrapper without .fsti, and bundle them:

krml -bundle 'Wrapper=Wrapper,Lib,Lib.Spec' Wrapper.krml Lib.krml Lib_Spec.krml
# Fatal error: exception Failure("nth")

After the fix, extraction succeeds and produces correct C output with all functions.

[protz]

• Are you doing separate extraction and compilation, or are we talking about a single run of krml?
• Can you show a complete example with the contents of Wrapper, Lib and Lib.Spec?
  Thanks

[protz]

@tahina-pro is this something you can help with? I would love for this PR to have a corresponding regression in the test suite, which would allow me to understand the problem -- right now, without a supporting example, it's hard to determine whether this is the right fix or not

[elefthei]

@protz hey sorry for dropping the ball this week is kind of busy. I will add a repro Friday

[protz]

Sorry for the delay -- got caught up with stuff then conference travel.

Ok, I was hoping you would give me a source .fst file rather than a .json. We do not have any JSON-based tests in the test suite right now, so this is a little strange.

Looking at it, I believe that the input ast that is being fed to krml is invalid: you are providing more naming hints than there are arguments in the function type for the external.

I would argue that this needs to be fixed upstream to trim the list of suggested names to at most the number of arrows in the type, but I would also take a patch in InputAstToAst that trims that list on the fly to avoid feeding an ill-formed ast into the pipeline. So, something like:

let t = mk_typ t in
let args, _ = flatten_arrow t in
let arg_names, _ = KList.split_at_nth (List.length args) in
DExternal2 ...

at line 53 of InputAstToAst.ml

Thanks!