Pulse.Lib.SpinLock C Extraction: Calling Convention Mismatch

## Summary

KaRaMeL generates calls to `acquire`/`release` with erased ghost
arguments that don't match the signatures in the shipped
`Pulse_Lib_SpinLock.h`. Users must write wrapper functions to bridge
the gap.

## Generated C (actual)

```c
Pulse_Lib_SpinLock_acquire((void *)0U, (void *)0U, lk);
Pulse_Lib_SpinLock_release((void *)0U, (void *)0U, lk);
```

## Shipped header (`dice/external/c/hacl/Pulse_Lib_SpinLock.h`)

```c
void Pulse_Lib_SpinLock_acquire(Pulse_Lib_SpinLock_lock l); // 1 arg
void Pulse_Lib_SpinLock_release(Pulse_Lib_SpinLock_lock l); // 1 arg
```

The two extra `(void *)0U` arguments are erased ghost parameters
(`#v:slprop` and `#p:perm`) that KaRaMeL doesn't fully erase.

## Minimal reproducer

### `spinlock-repro.fst`

```fstar
module SpinlockRepro

open Pulse.Lib.Pervasives
module L = Pulse.Lib.SpinLock
module B = Pulse.Lib.Box

#lang-pulse
fn protected_write (r: B.box int) (lk: L.lock)
requires L.lock_alive lk #1.0R (exists* v. B.pts_to r v)
ensures L.lock_alive lk #1.0R (exists* v. B.pts_to r v)
{
L.acquire lk;
B.op_Colon_Equals r 42;
L.release lk
}

#lang-pulse
fn main_fn ()
requires emp
ensures emp
{
let r = B.alloc #int 0;
let lk = L.new_lock (exists* v. B.pts_to r v);
protected_write r lk;
drop_ (L.lock_alive lk #1.0R (exists* v. B.pts_to r v))
}
```

### Steps to reproduce

```bash
# 1. Verify + extract to .krml
pulse --codegen krml --odir _build \
--extract 'krml:SpinlockRepro' spinlock-repro.fst

# 2. Run KaRaMeL
krml -skip-compilation -warn-error -2 \
-library Pulse.Lib.SpinLock \
-add-include '"Pulse_Lib_SpinLock.h"' \
-tmpdir _build \
$KARAMEL_HOME/krmllib/.extract/FStar_Pervasives_Native.krml \
$KARAMEL_HOME/krmllib/.extract/FStar_Pervasives.krml \
_build/SpinlockRepro.krml

# 3. Inspect generated C
cat _build/SpinlockRepro.c
```

### Full generated output

```c
void SpinlockRepro_protected_write(krml_checked_int_t *r,
Pulse_Lib_SpinLock_lock lk)
{
Pulse_Lib_SpinLock_acquire((void *)0U, (void *)0U, lk);
*r = (krml_checked_int_t)42;
Pulse_Lib_SpinLock_release((void *)0U, (void *)0U, lk);
}

void SpinlockRepro_main_fn(void)
{
krml_checked_int_t *r = KRML_HOST_CALLOC(1U, sizeof (krml_checked_int_t));
Pulse_Lib_SpinLock_lock lk = Pulse_Lib_SpinLock_new_lock();
SpinlockRepro_protected_write(r, lk);
}
```

Note that `new_lock()` is fine (0 args) but `acquire` and `release`
get 2 spurious `(void *)0U` arguments.

## Current workaround

Write a wrapper header that accepts and discards the ghost arguments:

```c
static inline void
Pulse_Lib_SpinLock_acquire(void *g1, void *g2,
Pulse_Lib_SpinLock_lock l) {
(void)g1; (void)g2;
Pulse_Lib_SpinLock_acquire_impl(l);
}
```

This shouldn't be necessary -- the shipped `.h`/`.c` should match
what KaRaMeL generates, or KaRaMeL should fully erase the ghost
parameters.

## Environment

- Pulse/F\*: 2025.12.15\~dev
- KaRaMeL: d7a8f9ec
- The shipped `Pulse_Lib_SpinLock.{h,c}` are at
`$PULSE_HOME/share/pulse/examples/dice/external/c/hacl/`

Start with the spinlock-repro.fst reproducer and run the listed pulse and krml commands to inspect the generated SpinlockRepro.c. Compare the acquire/release calls with dice/external/c/hacl/Pulse_Lib_SpinLock.h and its companion .c file. Done means the generated calls match the shipped one-argument declarations without wrapper functions.

Written by the indexing model from the issue text.