From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail-pg1-f175.google.com (mail-pg1-f175.google.com [209.85.215.175]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id B8B06381B05 for ; Thu, 19 Mar 2026 17:38:16 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.215.175 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1773941899; cv=none; b=EHTRR8E6/crBwgYkrjgNhh6lOtg//gcoPkfQzUFmkfdpZp46OB6qHH1Ggk1p8B0lihZv1TXdE53TgiDsUrYwoRQ0F6oZpzmy7A5lvmlqgP3NbmTiv8CTMZ+X4RiKQtmBlnBRLxpNuF60t9+RdFee+L/1yfT7Lin12jv5pLv1FMw= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1773941899; c=relaxed/simple; bh=iOKQxxTaVePDDINtdEVNa2vXNsDA0MBl/13v1fipV+c=; h=Message-ID:Subject:From:To:Cc:Date:In-Reply-To:References: Content-Type:MIME-Version; b=X8Q/HF+bntl43XEdMUIVyeUiLcu6pggt+WmolyX0vB/2N6t61dS1WkipO/hglsOPpml6LvmCaeQ0Gd5LK4iKHhNKxPTCmF0NRzZwpMFw9yI/4edZrxiH9k6Dvd1kGJhDqyaypGombpWMAzc0RagZ5tOOjTgcj/p5kFf8aDreHo0= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com; spf=pass smtp.mailfrom=gmail.com; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b=nkq7stBO; arc=none smtp.client-ip=209.85.215.175 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=gmail.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b="nkq7stBO" Received: by mail-pg1-f175.google.com with SMTP id 41be03b00d2f7-c06cb8004e8so400523a12.0 for ; Thu, 19 Mar 2026 10:38:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1773941896; x=1774546696; darn=vger.kernel.org; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc:subject :date:message-id:reply-to; bh=iOKQxxTaVePDDINtdEVNa2vXNsDA0MBl/13v1fipV+c=; b=nkq7stBOxp1p+dwZZROvJpWlDyx+lYxGZkzaZ9GBZQDfUAZ8ekfJwgvh+MHYKPucG4 vTR16Ur1oOJpFgnxlyxIlc0d8ojeklkfHgjV55bvvAeJQDRNje7w4nVcUwYudtptffYc 7nIzcDwLEvMqEVOcJjaG6FMSirjsMWGNACE7/qZrjWrGMoH92E6h8db6NwVQiLenuXXn lkL0c9HUAYnO7cdhMeMesd4pOqQJCb7jQwfcREOCRs1sgNovLng5W7s5otewjorYyRpV UpTFytwDBIU3VO5Ai/x7N15R2xccQQ9q6JZyDr3/Nq2sUdFpiQdL1h7vDyD5mMM6rAaH vFnw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1773941896; x=1774546696; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-gg :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=iOKQxxTaVePDDINtdEVNa2vXNsDA0MBl/13v1fipV+c=; b=ebmEuVALt3j9BAyHCurqzJBWZW9xUlSwWuMHQBfSbQjXsWINRT4J08fa9MDb9zWJ1H MF9eY+0HniFKvfy46klBtxzfZA3hbsy868XnfcKbXd51GiOfI/u0J0faF1b6obw+patt Uqi2VR006A/xgtk/JE25kP4VYxzNZ7P+kG5bWaP4s7ADjBC2IRrUSnZxg1Mgs+j8lX1u fIxdOZ/oS7BF2bW6UnWQV4EaCPvqdkXrvjwXSSaxWEs6/Yq3mcR1GfMAb5j4OF175Cem dkAaeodjwp++Fx6e9ywf7WcSx64auCYasZ4QGoD7H6/gtodKLsI1BkVfZKNKEB2CMf4+ tCSA== X-Forwarded-Encrypted: i=1; AJvYcCU9/egzNzJakwuW2DrxA4zAPKQkAE0HfKmNlEob/dgoJOcIJCFe4ZcoNDRWUzLebwSu5LJZ3Q7Jjg6rBmI=@vger.kernel.org X-Gm-Message-State: AOJu0YwKsJH/WwasHUzpr/IZLFA2Y25R0yPK5bTnBfK7kh4n04s1nEEM i49qzg8Cinxfzv7/lSwfjRI0w9/sdGHa4grq7AkGFWT3ee9idQkO4as4 X-Gm-Gg: ATEYQzwU5Q181RL4AqgvgOdbcOPUejxq5RBOh5JiYDJIzsQCB5euUrOd6CNnkTtN5Ww 1gMV7GmvR913H4spiwnwFPZf5pBYnoh7l7DnYgp/lLclsEOGcTkrPp+E+pDl3TDd3L2Bex8BU/w FvDWmch/C+EEG//Txa0Y45QGu93hXbuCRUYV92pDPJDCuvsYhmxVzjEeXw2wshQ08dJr+yu7w+5 AUncgF7VPIWUcpysEtB0VWFEAiOmjABiW4IW4KH2UFyeDjw2vBEaTDl5KWmGnMFXxXKUOGFgPm5 g+7ynVR5ZElZ2LzrCl4TuCtly4R2UUjxl2/ACkWmzw3smjoB2+ak9DsLGwddATS5IDotQgnnd8r eAN7nS0l1SWkGL8GRnT8WhcrQenai4DMcFeUyiz/tl46w51M8FKemioXofLvN/IxoAYHqxFQiSH jSOVgcX6SlFhjRu8V5AzcMEqQsx4+Oi2WkKIgtjat4eD2SxwJt0+AK+rVORVXMBQ== X-Received: by 2002:a05:6a20:d6c8:b0:398:79dc:eb59 with SMTP id adf61e73a8af0-39bcec302b7mr155374637.67.1773941895717; Thu, 19 Mar 2026 10:38:15 -0700 (PDT) Received: from [192.168.0.56] ([38.34.87.7]) by smtp.gmail.com with ESMTPSA id 41be03b00d2f7-c74453295a8sm33852a12.28.2026.03.19.10.38.15 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 19 Mar 2026 10:38:15 -0700 (PDT) Message-ID: <432750df75b5ce808f6b9ae9cd7ab3288a653b13.camel@gmail.com> Subject: Re: [PATCH] bpf: Simplify tnum_step() From: Eduard Zingerman To: Hao Sun , Kumar Kartikeya Dwivedi Cc: bpf@vger.kernel.org, ast@kernel.org, daniel@iogearbox.net, andrii@kernel.org, john.fastabend@gmail.com, martin.lau@linux.dev, linux-kernel@vger.kernel.org Date: Thu, 19 Mar 2026 10:38:12 -0700 In-Reply-To: References: <20260318171906.53174-1-hao.sun@inf.ethz.ch> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable User-Agent: Evolution 3.58.1 (3.58.1-1.fc43) Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 On Thu, 2026-03-19 at 10:06 +0100, Hao Sun wrote: > On Thu, Mar 19, 2026 at 9:18=E2=80=AFAM Kumar Kartikeya Dwivedi > wrote: > >=20 > > On Wed, 18 Mar 2026 at 19:21, Hao Sun wrote: > > > [...] > > > in case anyone is interested: > > > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 [1] https://pastebin.com/r= aw/czHKiyY0 > >=20 > > IMO it is worth it to include this proof inline in the commit log, > > since links are fragile. > > It's not that big, and I think it's more useful to have it inline than = not. > >=20 >=20 > The only concern is that the proof mainly uses `bv_decide`, which does no= t > provide much insight. But it's not big, I will inline it. I agree with you, not sure it would provide much signal, tbh. As far as I understand `bv_decide` means: SAT-solver, please do the magic := ) A more interesting discussion would be to have some model-checker based tests in the selftests, but Alexei was not excited last time we talked about that. If we have enough interested people, we can pick a checker and maintain a "shadow copy" of relevant functions and data structures in some repo e.g. on github + current proofs/tests. To have a starting point for future changes.