From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail-wm1-f41.google.com (mail-wm1-f41.google.com [209.85.128.41]) (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 26A563D47CF for ; Thu, 19 Mar 2026 13:24:19 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.128.41 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1773926660; cv=none; b=a0TdW9Gq48rsp8MeRFgu2EZOR0Cm4JY0+SB7iZtIJFFRhqoMgPApundB7DPieosr+DxW3jzEQYMxtuAj+9/Imsygoe3B/H6cZAmQh0ReyDXOgQ7Gnqi8CZRuIWxjZrZWR4oiBh4wwHWuxPmN9KyXVH7NnPdLKkD651c56Kg7a68= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1773926660; c=relaxed/simple; bh=1JjXQZ0Ix6V11YRCybUcCwN3aK889ehs17fGHxeZu6o=; h=Date:From:To:Cc:Subject:Message-ID:References:MIME-Version: Content-Type:Content-Disposition:In-Reply-To; b=dlXfd0rMDygkis+Q6ooNTtFosG89ISYw+eBRwWXhnzzUz/fKAdHzkF6CZqKxmgpdK2zsVXiftfsH4uMaRX+75wSOA86GwlPkSaztqZuFC8ZD1kLeL/9PNh9ZfyHC4nVwjzhiPBkV5BgpageHozw96FlCiksW8ecJYO/zZr3nezw= 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=Z1SySbQt; arc=none smtp.client-ip=209.85.128.41 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="Z1SySbQt" Received: by mail-wm1-f41.google.com with SMTP id 5b1f17b1804b1-486fb439299so5585265e9.0 for ; Thu, 19 Mar 2026 06:24:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1773926657; x=1774531457; darn=vger.kernel.org; h=in-reply-to:content-transfer-encoding:content-disposition :mime-version:references:message-id:subject:cc:to:from:date:from:to :cc:subject:date:message-id:reply-to; bh=d9SdmRpsBlveThR1KIVVShCqfmaw8QF26GnYrjY2FxE=; b=Z1SySbQt/w4psYJ085Wf9vCiDpbpKJnjftytDOVksQ+hbHhztK9igtRs+uAOQlT9u2 YvI0xyDKBBL4O2cqR7Z/EmgDfrgdJGAqk6eRYyk4827SsfM5w0+9mqa77ue8M/XD2oSt Cc6JV7UmtaSiTGaPZd06tVBpsWMimnFppiw8ovHfSVEPCWkL/Zy1LbFVZsTwyIjm90hc Wyuj5V45Dcu7+HZW8fFfmCxZi2S1WDHUjE+V9Umf017z+onfw5zv5QlSJNXaGq/Ns+zB 1o4u3UGhpnaCMHSwbJkisoIOK0SIyalU9dG3uyFOMpHX5y6W2Yi7eiEc4GX1UxpJsRs3 XJjQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1773926657; x=1774531457; h=in-reply-to:content-transfer-encoding:content-disposition :mime-version:references:message-id:subject:cc:to:from:date:x-gm-gg :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=d9SdmRpsBlveThR1KIVVShCqfmaw8QF26GnYrjY2FxE=; b=RQijJp3mQ3+nT3uuy7MYQFMzUlPfNX8m3E+5n+O1J7y24c8bPq9dzJ72bpP6/jqRWk 7N0oZ4usl+LKnhw015780kg8BOtp7trBH6/wC0IgLS3BC6TyqoWGzl/oHD3EcIdFYR2T GKAup+IswRnB71OwpBKlkQj5HFz2osk+Q6rT3kcKH1ceZjXrvnAbhmSIlwRWzUX6XNq5 ZDRl7ITA+5gNPk52mIIg27rCPffVAtz8zPEpBE13kM5zp/yV9Do0FrCD58LPDnO2ayAK Y+RlWWQh0jWvbn20uemOgSISXd3JGZ0Do764dH2MKyzzABEWHwA6OPsdHeIxPdHfDqEp PSmg== X-Forwarded-Encrypted: i=1; AJvYcCUGUH0iXOOeSqilDSyv4AW5aKOBK08NvbvukR2IaVwnfd3K8HsJ0gBJo655rRpxpz3ipUovM5GR6p9SLD8=@vger.kernel.org X-Gm-Message-State: AOJu0YybhwA8S9dDo2lCyC/R0aMLIFPMG3DcIMmPTqHwtiFSU8JhD9sB 5H3CdX6YWgkEkQ82eA4sSdVqvTdMn0Z+h2feZ0HW5rV7VhsMw8DJn3mX X-Gm-Gg: ATEYQzx4ZN0W6pZ0D9X78/M/Hs/WJ7hKZte+gBC+kMQzGJMUc3R2izJg589au0deI4I +ZHstEOU2qBZ/1sf6JYD14BcGBvmjrsbGU9SypxtW7V1nnqjJ5z7QKhCDP3Nm1iRmJlWrrutKhb ss6AUnzLMVhdZKrUx8cMUnOz+jxXljkD/iAfIps5phZvJh9VV/Oart/oYi8fuNjp6aNwd38XnNv 0m7Dt2IvVa1YEk9BEnJcehpJM0nnspPs2Hi1bqNvsGGMLSG6QnyK7cci/uAkphqL57+vAVomBLK mPVY9gKS1gxhlBiH9tL9KT44RlsrBCFnN5b3gUV/fsc0X7TiTF1FN/cEw8TikpqYQumvO687GXR fdzB11Z4mnH9mM1xouanVWjjej/Bl/lno/E/E6POfYpHr4qPe7ZXPHLzCjajaihGvWyq1fLmTxs ZQJbT4QTGfXnZbEl8ITcF6ZU7vjsNNtkksRfTZomy79/QWxLYPWVqVtpIFWQ5CIhuDoT0U/UN85 lCkuBU8khlgqkB60EyQ03D7txV/6AdTON/KCT/g+OaaNZz3FWwm3y+ZTymcyGI= X-Received: by 2002:a05:600c:1d10:b0:47e:e2eb:bc22 with SMTP id 5b1f17b1804b1-486f4421c84mr109885025e9.5.1773926657303; Thu, 19 Mar 2026 06:24:17 -0700 (PDT) Received: from mail.gmail.com (lfbn-ren-1-685-61.w81-53.abo.wanadoo.fr. [81.53.253.61]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-486f8bd5f7csm69524715e9.0.2026.03.19.06.24.16 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 19 Mar 2026 06:24:16 -0700 (PDT) Date: Thu, 19 Mar 2026 14:24:14 +0100 From: Paul Chaignon To: Hao Sun Cc: Shung-Hsi Yu , Harishankar Vishwanathan , bpf@vger.kernel.org, ast@kernel.org, daniel@iogearbox.net, andrii@kernel.org, eddyz87@gmail.com, john.fastabend@gmail.com, martin.lau@linux.dev, linux-kernel@vger.kernel.org Subject: Re: [PATCH] bpf: Simplify tnum_step() Message-ID: References: <20260318171906.53174-1-hao.sun@inf.ethz.ch> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: On Thu, Mar 19, 2026 at 02:12:54PM +0100, Hao Sun wrote: > On Thu, Mar 19, 2026 at 10:35 AM Paul Chaignon wrote: > > > > On Thu, Mar 19, 2026 at 10:01:31AM +0100, Hao Sun wrote: > > > > Thanks for the cc Shung-Hsi. We were discussing it with Hari who's > > planning to double check soundness. > > Great, let me know the result when the verification is done; I will then > send the v2. > > > > > > [...] > > > > > - res = w; > > > > > - } > > > > > - return res; > > > > > + d = z - t.value; > > > > > > > > A bit of comment explaining would be nice. > > > > > > > > > > The commit message is self-contained; anyone interested can git blame. > > > But I am unsure. If a detailed description is preferred, I can add a > > > comment to v2. > > > > Not disagreeing about the role of git blame, but it's not a replacement > > for code comments either. Having just the intuition in comments can help > > a lot; as you mention below, it's one less indirection ;) > > > > In its current form, I find the proof harder to follow than the > > previous, very verbose version. Maybe there's a good middle ground? > > > > By `proof`, you are referring to the description/commit message, not > the Lean4 proof, right? I was a bit confused here. Seems I thought one word and wrote another :/ I meant the code, the tnum_step function. > > [...]