From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id kJnYIEUD1mHrjAAAgWs5BA (envelope-from ) for ; Wed, 05 Jan 2022 21:44:53 +0100 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id OMgxHkUD1mHdeAEA9RJhRA (envelope-from ) for ; Wed, 05 Jan 2022 21:44:53 +0100 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id DCD743EA7E for ; Wed, 5 Jan 2022 21:44:52 +0100 (CET) Received: from localhost ([::1]:44220 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1n5D9P-00011O-UU for larch@yhetil.org; Wed, 05 Jan 2022 15:44:51 -0500 Received: from eggs.gnu.org ([209.51.188.92]:52384) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1n5D8S-0007qS-GD for guix-devel@gnu.org; Wed, 05 Jan 2022 15:43:52 -0500 Received: from [2a00:1450:4864:20::343] (port=53946 helo=mail-wm1-x343.google.com) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1n5D8Q-0002rl-Ny for guix-devel@gnu.org; Wed, 05 Jan 2022 15:43:52 -0500 Received: by mail-wm1-x343.google.com with SMTP id l4so455238wmq.3 for ; Wed, 05 Jan 2022 12:43:49 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=message-id:subject:from:to:date:in-reply-to:references:user-agent :mime-version:content-transfer-encoding; bh=uvAovfodizDU9JU1QD3hFxDN1wByhEI7LncRpdcen/0=; b=ayZdXQhUjNYnU9i5mZu5Uv9EX+o30SWd1uWVp9pLXis8IhgqkTciQBxx9zL2sIBF9D HGuMCAdzCSij7aFUMvGiM7ke/56w5qFU/EO0LUilAfHct7pqJvYgPxCoZsXfDyPkOAcZ 3olo8ARxboOo6aTDIKStcqxHNYj5LCnyFnlUMU+Z9hZrX/v2Y0Fau5zu8SJO3rvqK8wV eiGmPRic8Qd5awgGXA6jOCTyfQKB3y3B0U9zCBLji+Y5BmUHNUcX+2h6e9k2ELXYfeep o2pOqCbhzOSvckkDQmAEWe/7z3GsX0aIKF5qeslK0rqv4eYqd/Zd1+hus0RHcECQPAoo TtbA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:message-id:subject:from:to:date:in-reply-to :references:user-agent:mime-version:content-transfer-encoding; bh=uvAovfodizDU9JU1QD3hFxDN1wByhEI7LncRpdcen/0=; b=aKQEfo1cteKdYmjzrhTCdlzsvQ4nppQo7YG6RMyoC2GEvv85raYuEcuQbgNTMggcMg Pdw6S7U8FHmO4zphA4jIQwhF7u5ZTq9dZr6/ruZZ1zppBBiPxnBF9175voWTgbLmDH5f ZIEp3XJf6k52OnWcoLnrsdcC+ury6zCGLi/iyWFwI+NEdR/3H5xdGMrv1STPKb6HgR01 vCXZrxXRjqb0jy/kXuVIsdYC7LCboTtv9JGrqWwinmGJdiRnGutP77VEFw3LUCVOU/q0 QWsLJ0rHMyahhdDlcep5mPQ0Tga+eXaTBlVaC7pviSYsNXQa3Bz8KMefXrX8WmGEexwT wEzQ== X-Gm-Message-State: AOAM532c6o/CnQTA9bOPum9dwuRtLQ+jsHVILwFdXhtiqP77/U4PRG0P zAEFycw43drctyz3E2wojN8= X-Google-Smtp-Source: ABdhPJyG32sIRM1tybAZBMpcre8PvOWcQ/BzCHivAKZYJSmkyU4XVWITtoR/mvc2lL6VFDziwOHwNA== X-Received: by 2002:a05:600c:643:: with SMTP id p3mr4329843wmm.130.1641415428107; Wed, 05 Jan 2022 12:43:48 -0800 (PST) Received: from nijino.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id l26sm3411495wme.36.2022.01.05.12.43.46 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 05 Jan 2022 12:43:47 -0800 (PST) Message-ID: <47d713d7bbfb4673c25398e0d6c62a47b4f490f4.camel@gmail.com> Subject: Re: On raw strings in commit field From: Liliana Marie Prikler To: Mark H Weaver , zimoun , guix-devel@gnu.org Date: Wed, 05 Jan 2022 21:43:46 +0100 In-Reply-To: <87h7aia5ug.fsf@netris.org> References: <6e451a878b749d4afb6eede9b476e5faabb0d609.camel@gmail.com> <86y243kdoo.fsf@gmail.com> <899587fb6a76ddfa37d197d3d0fd23cdc7ad8592.camel@gmail.com> <867dbmi7pf.fsf@gmail.com> <3d448fe42f0c43574db96fa26aecd7da5fd5a95d.camel@gmail.com> <877dbkmjm9.fsf@netris.org> <762e9fb7116c442bf0f8f63221bf32fa2b77f2cf.camel@gmail.com> <87y240kq2i.fsf@netris.org> <9362c6fb7e34ded5d009c3f79cd18300d6cd539c.camel@gmail.com> <87r19rkx9h.fsf@netris.org> <87r19pbv8y.fsf@netris.org> <87mtkcbedc.fsf@netris.org> <3f947861672144d202a8c736d5e8f2b905c31b66.camel@gmail.com> <871r1nawz8.fsf@netris.org> <87h7aia5ug.fsf@netris.org> Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.42.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Host-Lookup-Failed: Reverse DNS lookup failed for 2a00:1450:4864:20::343 (failed) Received-SPF: pass client-ip=2a00:1450:4864:20::343; envelope-from=liliana.prikler@gmail.com; helo=mail-wm1-x343.google.com X-Spam_score_int: -12 X-Spam_score: -1.3 X-Spam_bar: - X-Spam_report: (-1.3 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RDNS_NONE=0.793, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no X-Spam_action: no action X-BeenThere: guix-devel@gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+larch=yhetil.org@gnu.org Sender: "Guix-devel" X-Migadu-Flow: FLOW_IN X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1641415493; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references:list-id:list-help: list-unsubscribe:list-subscribe:list-post:dkim-signature; bh=uvAovfodizDU9JU1QD3hFxDN1wByhEI7LncRpdcen/0=; b=iVoIsao4aUk13YKaf6uxq3QcCkFVkDArc6rWB4KfF5UAnEMBidlwQXUv4tNQ97jsigy1gU 0XRhL23goVIo56DZw4vn5BiU44sKBijoHaGJmPzHP7AB2BcXQcU7nivNBwG085hSy7bZIP McaaQKfvK/bYGgLuCrUyc/c86qj5JjqnUH9AK1M1dUFuKfVlu5RjSf19+00NdqTSqCv9aW ZTSJOR2eYlluq20+GrZ26+kyn+rnAPsFdFNVbBzQIuiJY075hAz7f5NGNYDtz8iDMBXmQp CYotkD4NZ6ICED+Py75v3rh8Z5mAR1kSDPEepdVk777QcXyHe658Ll2Q/j1KMg== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1641415493; a=rsa-sha256; cv=none; b=EAR8O6r13SCT7+Ia6sCXr6BKlFONQ0pJv/18+snOWKEHcZTu41zKG9pdHKSbp+E5qgSPSC 0oxSqLe5MuUUJJ2diQNPTykSMFMr/sSl8tMvWA/1e4LKPFZ6saQODfxHJNALV5c8rafrb8 0cJ93WlQgZjZYkjYwl5gsZJA4p7yigayQsyaOMIUciiEuYyeDJ4hmNd+W7S6kvLQWtvJPu ipSWR81AmSUqZfSeDsul2Ye1F654CHTTTxtM6B/h6jOae2eOerRhcirD8PnTPNSwPdnJRd VNX5rx57p+QhmFjPwMICS7uR4x1xCkr1dXYnErMn3dA1Ywh2huSNGZiDxA1p/w== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=gmail.com header.s=20210112 header.b=ayZdXQhU; dmarc=pass (policy=none) header.from=gmail.com; spf=pass (aspmx1.migadu.com: domain of "guix-devel-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-devel-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: -4.80 Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=gmail.com header.s=20210112 header.b=ayZdXQhU; dmarc=pass (policy=none) header.from=gmail.com; spf=pass (aspmx1.migadu.com: domain of "guix-devel-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-devel-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: DCD743EA7E X-Spam-Score: -4.80 X-Migadu-Scanner: scn0.migadu.com X-TUID: 3JGH0E/qBjMT Am Mittwoch, dem 05.01.2022 um 04:28 -0500 schrieb Mark H Weaver: > Hi Liliana, > > Earlier, I wrote: > > Sorry, but this is not even close to a valid argument that the set > > of possible push actions to a Git repo is uncountable.  In fact, > > it's quite easy to prove that the set is countable.  Any > > mathematician will know this. > > I suppose I should give a proof.  I'll give two proofs. Now, those two proofs are nice and I'm not going to dispute them. However, just for the record I do think that you're paying a little too much attention to formalisms and too little to everything else I'm saying. In the case of Cantor vs. the liar paradox (which I've wrongly attributed to Cantor because his proof is being used in Gödel's incompleteness theorem and the Halting Problem¹), that's completely on me, although I'm not sure whether that suffices for gaslighting. In any case, it was not intentional. In this context, on the other hand, it ought to have been comparatively easy to infer that I was talking about push actions (plural) as sequences, not as individual push actions like you've used for your proof. >From here on, I will assume that each individual push action is finite as you did, but I don't think that using communications of finite length are a helpful building block here. Porting Git to Turing Machines would have the effect of allowing an infinite tape shared between multiple machines and they could possibly run forever. However, I am going to assume that each individual push action is finite anyway, as your assumptions will typically hold for reasons of practicability. Note, though, that this would not suffice for robustness arguments. Whatever communications you make at a given time, you can not be sure that your observations will be replicated if you repeat them (even if restricted to fetching only). As we're trying to generalize your proof for a single push action to be chosen among a finite set to all communications to a series of push actions, we do encounter a problem if we were to encode this as a mere list of push actions. This can be done by a rather simple Cantor proof: The set of lists of a particular type T which admits at least two values is uncountable (a list of booleans can be directly mapped to a binary number and thus Cantor's original proof applied). Since there are more than two permissible push actions, we have a problem. Luckily, there is a straightforward solution. A push action can only create new commits (of which there are finitely many, both in terms of the content committed as per your argument as in their count by the limited number of SHA-1 hashes), create new branches (which must have a finitely long name as per your argument), or create tags (which also must have finitely long names, again per your argument). There are no other operations worth mentioning and a push action must contain at least one action to be valid. Therefore, a valid sequence of push actions is finite, as it will inevitably end up using all SHA-1 hashes as well as all possible branch and tag names in some configuration. Q.E.D. Remember the ¹ I wrote earlier? Now originally, I had planned to write a formal proof to show how validating a tag (i.e. making sure it does not get assigned to a different commit) and likewise validating a commit after SHA-whateverthenextattackwillbenamed would be co-RE-hard. It would likely have invoked Cantor at some point, though again perhaps at a lower level than you'd have liked. But I am sure you agree, that this proof that Git is completely safe, actually, is much nicer. There shouldn't be anything that could discredit it, least of all something past me would have said. WDYT?