From f6eb5f5aabc6e1d0f8622d557204a85afaa85192 Mon Sep 17 00:00:00 2001
From: T Savo <evilgenius@nefariousplan.com>
Date: Wed, 27 May 2026 05:35:56 -0700
Subject: [PATCH] feat(lift-go): lift leading guard-panics into preconditions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The Go production lifter emitted `pre = true` for every function — a
consumer's defensive guard (`if !P(args){panic}`) never became a contract
precondition, so it was invisible at call sites. This brings Go to parity
with the Rust (lift_function_precondition) and C# (LiftMethodPrecondition)
walkers: a leading `if !P{panic}` lifts to `pre = P == true`, a bare
`if cond{panic}` to `cond == false`.

Scans only leading guards, stops at the first non-guard statement, and
refuses to invent a precondition from an unliftable condition. CID-neutral
for existing kits (the Go self-contracts contractSetCid is unchanged —
073e4010…; no go-kit function uses the guard pattern). Lifter tests pass.

Unblocks the BZ-DETERMINISM-001 reference species: a consumer's
canonical-byte-order precondition now lifts from idiomatic Go.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---
 implementations/go/provekit-lift-go/lift.go | 62 ++++++++++++++++++++-
 1 file changed, 61 insertions(+), 1 deletion(-)

diff --git a/implementations/go/provekit-lift-go/lift.go b/implementations/go/provekit-lift-go/lift.go
index a6250df88..32ac63e61 100644
--- a/implementations/go/provekit-lift-go/lift.go
+++ b/implementations/go/provekit-lift-go/lift.go
@@ -316,7 +316,7 @@ func liftFunc(fset *token.FileSet, file *ast.File, pkg *types.Package, info *typ
 	if err != nil {
 		return FunctionContract{}, nil, refuse("unsupported-syntax", errPos(err, fn.Pos()), err.Error())
 	}
-	pre, err := formulaValue(ir.And())
+	pre, err := formulaValue(l.liftLeadingGuardPreconditions(fn.Body.List))
 	if err != nil {
 		return FunctionContract{}, nil, refuse("internal-error", fn.Pos(), err.Error())
 	}
@@ -353,6 +353,66 @@ func liftFunc(fset *token.FileSet, file *ast.File, pkg *types.Package, info *typ
 	return contract, body.term, nil
 }
 
+// liftLeadingGuardPreconditions lifts a function's leading defensive guards
+// (`if <cond> { panic(...) }`) into a precondition. A guard panics when <cond>
+// holds, so the caller's obligation to avoid the panic is ¬<cond>. This brings
+// the Go production lifter to parity with the Rust (lift_function_precondition)
+// and C# (LiftMethodPrecondition) walkers; without it every function lifted
+// `pre = true`, so a consumer's defensive contract was invisible at call sites.
+// Scans only leading guards and stops at the first non-guard statement, so it
+// never fabricates a precondition from arbitrary control flow.
+func (l *lifter) liftLeadingGuardPreconditions(stmts []ast.Stmt) ir.IrFormula {
+	var atoms []ir.IrFormula
+	for _, stmt := range stmts {
+		ifStmt, ok := stmt.(*ast.IfStmt)
+		if !ok || ifStmt.Init != nil || ifStmt.Else != nil || !isPanicOnlyBlock(ifStmt.Body) {
+			break
+		}
+		atom, ok := l.guardPreconditionAtom(ifStmt.Cond)
+		if !ok {
+			break
+		}
+		atoms = append(atoms, atom)
+	}
+	return ir.And(atoms...)
+}
+
+// guardPreconditionAtom lifts ¬cond as a precondition atom. `if !P { panic }`
+// lifts to the clean `P == true`; a bare `if cond { panic }` lifts to
+// `cond == false`. Returns false when the condition is not liftable, so the
+// caller refuses to invent a precondition rather than emit a wrong one.
+func (l *lifter) guardPreconditionAtom(cond ast.Expr) (ir.IrFormula, bool) {
+	if unary, ok := cond.(*ast.UnaryExpr); ok && unary.Op == token.NOT {
+		inner, err := l.liftExpr(unary.X)
+		if err != nil {
+			return nil, false
+		}
+		return ir.Eq(inner.term, ir.BoolConst(true)), true
+	}
+	lifted, err := l.liftExpr(cond)
+	if err != nil {
+		return nil, false
+	}
+	return ir.Eq(lifted.term, ir.BoolConst(false)), true
+}
+
+// isPanicOnlyBlock reports whether a block is exactly `{ panic(...) }`.
+func isPanicOnlyBlock(b *ast.BlockStmt) bool {
+	if b == nil || len(b.List) != 1 {
+		return false
+	}
+	exprStmt, ok := b.List[0].(*ast.ExprStmt)
+	if !ok {
+		return false
+	}
+	call, ok := exprStmt.X.(*ast.CallExpr)
+	if !ok {
+		return false
+	}
+	ident, ok := call.Fun.(*ast.Ident)
+	return ok && ident.Name == "panic"
+}
+
 func extractFormals(info *types.Info, fn *ast.FuncDecl) ([]string, []any, map[types.Object]bool, error) {
 	locals := map[types.Object]bool{}
 	var names []string