square(x) := x*x
law square(-x) == square(x)

A law states a property once. Its assurance rises without touching the source.

law::verify(code) runs tested → proved and returns a LawReport per law. CLI: warp verify file.wasp (or inline code) prints the reports and exits 1 if any law is violated.

• Warp Int promotes to arbitrary precision: square(3037000500) is 9223372037000250000. It is exported as Lean Int, so Proved means proved for Warp's mathematical integer semantics. Explicit as i64 values still wrap, but casts are not exported yet.
• Definitions use def f (x : Int) : Int := …. The Lean term covers + - * %, ^n with a literal nonnegative exponent, unary minus, ?:, if then else, and comparisons (lifted to 0/1 inside terms). % uses Int.tmod, matching signed truncating remainder. Warp / yields a Float, so it isn't exported.
• The law becomes theorem f_law (vars : Int) : prop := by try simp only [defs]; all_goals first | (t; done) | …. Every tactic is wrapped in ; done because simp can rewrite a goal without closing it and still count as success.
• Tactics are core Lean only: rfl decide ac_rfl grind simp, plus a small checked helper for 0 ≤ x*x; no Mathlib is required. Unlike finite BitVec, arbitrary Int cannot be exhaustively decided. A law that generated tests do not refute and Lean cannot prove therefore remains Tested/Unknown rather than producing a spurious finite-word counterexample.
• Results are cached by the hash of the Lean source in target/lean/law_<hash>.{lean,result}. This is the "proof result recorded" step until the semantic artifact exists.
• Recursive functions are proved by induction over their own recursion: the function is exported with the sum of its parameters' sizes as termination measure, and the recursive call is the induction hypothesis.
• A law proved before is a lemma of the laws after it. fact(n) > 0 stays Tested alone; with a helper law first, both are Proved:

  fact(n) := if n <= 0 then 1 else n * fact(n - 1)
  law x > 0 and y > 0 => x * y > 0
  law fact(n) > 0
  

• Not exported, so the law stays at the Tested level: Float parameters, /, and anything outside the term subset.

• Proved: Lean closed the goal.
• FAILED … counterexample x=1: a property test instance evaluated to false.
• Tested (reason): every generated instance held, but Lean could not prove it or export it.

Counterexamples come from property tests evaluated in wasm. Lean either proves the universal integer statement or returns Unknown.

• Laws caught a real bug: in := functions, x:float parameters are compiled as Int, so half(x:float) := x/2; half(1.0) returns 0. See the ignored test test_law_float_parameters_are_tested. The cause is that UserFunctionDef.params keeps only defaults, not types, and infer_function_return_kind assumes Int.

Bend 2 (HigherOrderCO, Victor Taelin) states laws the same way: law name: for x: T {lhs == rhs}, proved by a def of the same name (reflexivity, rewrites, a recursive call as the induction hypothesis), checked by its Lean-verified kernel BendTT. Its project convention, a LAWS file the human writes and a PROOF file the AI writes, with ALL PROOFS CHECK as the gate, is the model for warp's next steps: the for x: T quantifier and proofs as defs for recursive functions, which the Lean export skips today. Ideas taken, no code copied.

• Attach laws to FunctionDecl in src/semantic/ once that IR exists. Persist the verdict in the Wasp-serialized artifact instead of target/lean.
• Use an SMT backend (z3 is installed) as a faster prover for linear and bitvector laws.
• Asserted mode checks concrete call sites at compile time. It doesn't yet check values computed at runtime inside the WASM module.
• Lawful lifting: broadcasting is allowed only where functor laws are Proved.