fix: keep unit argument for specs instead of dropping them

fork/patches/hax-specs.md

@@ -21,6 +21,8 @@ are consumed by the producer.
 - Without `-specs`, the output is unchanged and the prepass is a no-op.
 - Decoration functions never appear as such; only as `<fn>.pre`/`<fn>.post`.
 - Arguments of spec functions are printed with `Extract.extract_App` (#58).
+- Specs and obligations pass every input of the function, in order: unit
+  inputs, which are extracted as `_` binders, are passed as `()` (#79).
 - Obligations are plain theorems, not `@[spec]` lemmas: users register the
   specs they prove.
 - Spec and obligation files are emitted only when non-empty; their imports come
@@ -32,7 +34,7 @@ are consumed by the producer.
 
 - `tests/src/hax_specs` (expected outputs `tests/lean/HaxSpecs`): basic specs,
   const and trait generics, `future`, implicit generics, mutually recursive
-  functions.
+  functions, unit arguments (#79).
 - The `hax-lib` crates are vendored for the nix check (`haxSpecsVendor` in
   `flake.nix`).
 
@@ -46,3 +48,4 @@ are consumed by the producer.
 - 2026-10-23: the `step`-style backend (`-specs hax-step`, its test
   `tests/src/hax_specs_step` and the `@[spec]` attribute on obligations) removed
   (fork PR #76).
+- 2026-10-23: unit arguments are kept in specs and obligations (fork PR #79).

src/extract/ExtractHaxSpecs.ml

@@ -46,6 +46,17 @@ module Helpers = struct
     let id = Pure.FunOrOp (Fun (FromLlbc (FunId id, None))) in
     { e = Qualif { id; generics }; ty }
 
+  (** The arguments passed for the input patterns of a function. Unit inputs are
+      [_] (see [unit_vars_to_unit]): we pass them as [()]. *)
+  let input_args span (inputs : Pure.tpat list) : Pure.texpr list =
+    List.map
+      (fun (p : Pure.tpat) ->
+        match PureUtils.tpat_to_texpr span p with
+        | Some e -> e
+        | None when p.ty = PureUtils.mk_unit_ty -> PureUtils.mk_unit_texpr
+        | None -> [%internal_error] span)
+      inputs
+
   (** Emit [(<cond> <generics> <args>).holds] for a fn [f]. *)
   let emit_holds span ctx fmt generics args (f : Pure.fun_decl) =
     let head = fun_head f.def_id generics f.signature.output in
@@ -184,8 +195,7 @@ let emit_spec ctx fmt (s : HaxSpecs.spec) opt_span =
           let arg_texprs =
             match parent.body with
             | None -> []
-            | Some { inputs; _ } ->
-                List.filter_map (PureUtils.tpat_to_texpr span) inputs
+            | Some { inputs; _ } -> input_args span inputs
           in
           (* Fresh result-var id, from the body generator so it can't clash. *)
           let res_id = fresh_fvar_id () in
@@ -264,8 +274,7 @@ let emit_obligation ctx fmt (o : HaxSpecs.obligation) opt_span =
           let arg_texprs =
             match parent.body with
             | None -> []
-            | Some { inputs; _ } ->
-                List.filter_map (PureUtils.tpat_to_texpr span) inputs
+            | Some { inputs; _ } -> input_args span inputs
           in
 
           (* Blank line before the entry. *)

tests/lean/HaxSpecs/HaxSpecs.lean

@@ -201,6 +201,33 @@ partial_fixpoint
 
 end
 
+/-- Trait declaration: [hax_specs::unit_args::Size]
+    Source: 'src/lib.rs', lines 197:4-199:5 -/
+structure unit_args.Size (Self : Type _) where
+  len : Self → RustM Std.Usize
+
+/-- [hax_specs::unit_args::{impl hax_specs::unit_args::Size for ()}::len]:
+    Source: 'src/lib.rs', lines 205:8-207:9 -/
+def Tuple.Insts.Hax_specsUnit_argsSize.len (_ : Unit) : RustM Std.Usize := do
+  ok 0#usize
+
+/-- Trait implementation: [hax_specs::unit_args::{impl hax_specs::unit_args::Size for ()}]
+    Source: 'src/lib.rs', lines 203:4-208:5 -/
+@[reducible]
+def Tuple.Insts.Hax_specsUnit_argsSize : unit_args.Size Unit := {
+  len := Tuple.Insts.Hax_specsUnit_argsSize.len
+}
+
+/-- [hax_specs::unit_args::named]:
+    Source: 'src/lib.rs', lines 211:4-213:5 -/
+def unit_args.named (_ : Unit) : RustM Std.Usize := do
+  ok 0#usize
+
+/-- [hax_specs::unit_args::before_other]:
+    Source: 'src/lib.rs', lines 218:4-220:5 -/
+def unit_args.before_other (_ : Unit) (y : Std.U32) : RustM Std.U32 := do
+  ok y
+
 
 /-- [hax_specs::basic::only_requires::pre]:
     Source: 'src/lib.rs', lines 5:4-5:24 -/
@@ -543,6 +570,38 @@ def mutual.is_odd.spec (n : Std.U32) : Prop :=
   ⦃ ⇓ res => ⌜ (mutual.is_odd.post n res).holds ⌝ ⦄
 
 
+/-- [hax_specs::unit_args::named::post]:
+    Source: 'src/lib.rs', lines 210:4-210:36 -/
+@[reducible]
+def unit_args.named.post (_ : Unit) (result : Std.Usize) : RustM Bool := do
+  ok (result = 0#usize)
+
+def unit_args.named.spec (_ : Unit) : Prop :=
+  ⦃ ⌜ True ⌝ ⦄
+  unit_args.named ()
+  ⦃ ⇓ res => ⌜ (unit_args.named.post () res).holds ⌝ ⦄
+
+
+/-- [hax_specs::unit_args::before_other::pre]:
+    Source: 'src/lib.rs', lines 216:4-216:24 -/
+@[reducible]
+def unit_args.before_other.pre (_ : Unit) (y : Std.U32) : RustM Bool := do
+  ok (y < 100#u32)
+
+/-- [hax_specs::unit_args::before_other::post]:
+    Source: 'src/lib.rs', lines 217:4-217:36 -/
+@[reducible]
+def unit_args.before_other.post
+  (_ : Unit) (y : Std.U32) (result : Std.U32) : RustM Bool := do
+  ok (result = y)
+
+def unit_args.before_other.spec (_ : Unit) (y : Std.U32) : Prop :=
+  (unit_args.before_other.pre () y).holds →
+  ⦃ ⌜ True ⌝ ⦄
+  unit_args.before_other () y
+  ⦃ ⇓ res => ⌜ (unit_args.before_other.post () y res).holds ⌝ ⦄
+
+
 /-- [hax_specs::const_generic_ty::{hax_specs::const_generic_ty::MyStruct<N>}::build::pre]:
     Source: 'src/lib.rs', lines 121:8-121:28 -/
 @[reducible]
@@ -583,6 +642,18 @@ def const_generic_ty.MyStruct.get.spec {N : Std.Usize}
   ⦃ ⇓ res => ⌜ (const_generic_ty.MyStruct.get.post self res).holds ⌝
   ⦄
 
+
+/-- [hax_specs::unit_args::{impl hax_specs::unit_args::Size for ()}::len::post]:
+    Source: 'src/lib.rs', lines 204:8-204:28 -/
+@[reducible]
+def unit_args.SizeTuple.len.post (_ : Unit) (i : Std.Usize) : RustM Bool := do
+  ok true
+
+def Tuple.Insts.Hax_specsUnit_argsSize.len.spec (_ : Unit) : Prop :=
+  ⦃ ⌜ True ⌝ ⦄
+  Tuple.Insts.Hax_specsUnit_argsSize.len ()
+  ⦃ ⇓ res => ⌜ (unit_args.SizeTuple.len.post () res).holds ⌝ ⦄
+
 theorem basic.only_requires.spec.proof (x : Std.U32) :
   basic.only_requires.spec x
   := by sorry
@@ -646,6 +717,13 @@ theorem mutual.is_even.spec.proof (n : Std.U32) : mutual.is_even.spec n
 theorem mutual.is_odd.spec.proof (n : Std.U32) : mutual.is_odd.spec n
   := by sorry
 
+theorem unit_args.named.spec.proof (_ : Unit) : unit_args.named.spec ()
+  := by sorry
+
+theorem unit_args.before_other.spec.proof (_ : Unit) (y : Std.U32) :
+  unit_args.before_other.spec () y
+  := by sorry
+
 theorem const_generic_ty.MyStruct.build.spec.proof (N : Std.Usize)
   (k : Std.Usize) : const_generic_ty.MyStruct.build.spec N k
   := by sorry
@@ -655,4 +733,8 @@ theorem const_generic_ty.MyStruct.get.spec.proof {N : Std.Usize}
   const_generic_ty.MyStruct.get.spec self
   := by sorry
 
+theorem Tuple.Insts.Hax_specsUnit_argsSize.len.spec.proof (_ : Unit) :
+  Tuple.Insts.Hax_specsUnit_argsSize.len.spec ()
+  := by sorry
+
 end hax_specs

tests/src/hax_specs/src/lib.rs

@@ -187,3 +187,35 @@ mod mutual {
         if n == 0 { false } else { is_even(n - 1) }
     }
 }
+
+// Unit arguments are extracted as `_` binders: the specs must still pass them,
+// as `()`.
+#[allow(dead_code)]
+mod unit_args {
+    use hax_lib::*;
+
+    trait Size {
+        fn len(&self) -> usize;
+    }
+
+    // `self : ()`
+    #[hax_lib::attributes]
+    impl Size for () {
+        #[ensures(|_| true)]
+        fn len(&self) -> usize {
+            0
+        }
+    }
+
+    #[ensures(|result| result == 0)]
+    fn named(x: ()) -> usize {
+        0
+    }
+
+    // The unit argument comes before another one.
+    #[requires(y < 100)]
+    #[ensures(|result| result == y)]
+    fn before_other(x: (), y: u32) -> u32 {
+        y
+    }
+}