From beead0a3ebc977819630837e47a836b1303a94bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 30 Sep 2026 17:41:10 +0200 Subject: [PATCH] fix: keep unit argument for specs instead of dropping them Fork-Patch: hax-specs --- fork/patches/hax-specs.md | 5 +- src/extract/ExtractHaxSpecs.ml | 17 +++++-- tests/lean/HaxSpecs/HaxSpecs.lean | 82 +++++++++++++++++++++++++++++++ tests/src/hax_specs/src/lib.rs | 32 ++++++++++++ 4 files changed, 131 insertions(+), 5 deletions(-) diff --git a/fork/patches/hax-specs.md b/fork/patches/hax-specs.md index f38634b1b..04bd0e9c5 100644 --- a/fork/patches/hax-specs.md +++ b/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 `.pre`/`.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). diff --git a/src/extract/ExtractHaxSpecs.ml b/src/extract/ExtractHaxSpecs.ml index b58ac3780..06178d429 100644 --- a/src/extract/ExtractHaxSpecs.ml +++ b/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 [( ).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. *) diff --git a/tests/lean/HaxSpecs/HaxSpecs.lean b/tests/lean/HaxSpecs/HaxSpecs.lean index 826b0d2aa..3af4cb499 100644 --- a/tests/lean/HaxSpecs/HaxSpecs.lean +++ b/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}::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 diff --git a/tests/src/hax_specs/src/lib.rs b/tests/src/hax_specs/src/lib.rs index 6a5700e8c..396f7b8a8 100644 --- a/tests/src/hax_specs/src/lib.rs +++ b/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 + } +}