MIME-Version: 1.0
References: 
 <CAA1-vB0H9ytS8Af-E7rL3-2XjDFKKiP5AgXL=NVJSvCzc+5VQQ@mail.gmail.com>
 <CAPeSryro49=BNuocgU+ULDh0W++4VuHpywivxicdu5GQFAyHjQ@mail.gmail.com>
In-Reply-To: 
 <CAPeSryro49=BNuocgU+ULDh0W++4VuHpywivxicdu5GQFAyHjQ@mail.gmail.com>
From: Prachi Jain <prachi.jain1288@gmail.com>
Date: Thu, 16 Jul 2026 08:59:39 -0500
Message-ID: 
 <CAA1-vB1+Jm2omHgYwUKd6rkFyNRSEUG1ubUk_tXzk82XBOBakw@mail.gmail.com>
To: Felix Linker <linkerfelix@gmail.com>
Content-Type: multipart/alternative; boundary="000000000000a9f5120656badac0"
Message-ID-Hash: TFT3VFYHBIAP7TUPALM4TFETXP3EHOW7
CC: keytrans@ietf.org
Precedence: list
Subject: =?utf-8?q?=5BKeytrans=5D_Re=3A_Keytrans=40IETF_126_=3A_Call_for_agenda_topic?=
	=?utf-8?q?s?=
Archived-At: 
 <https://mailarchive.ietf.org/arch/msg/keytrans/P05X5x1o_ux3IvSY-ujifWD9xp4>

--000000000000a9f5120656badac0
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Thanks for sharing this, Felix. We will put you on the agenda.

On Thu, Jul 16, 2026 at 3:14=E2=80=AFAM Felix Linker <linkerfelix@gmail.com=
> wrote:

> Hi Prachi and fellow keytrans enthusiasts,
>
> We made progress implementing a client. The client is still very much WIP=
,
> but I believe (with an asterisk) that it should be able to verify greates=
t
> version queries.
>
> The code for that can be found here:
> https://github.com/felixlinker/keytrans-verification/blob/felixlinker/cli=
ent-state/pkg/client/client.go#L98
> Development currently happens on that branch.
>
> I could not test whether the client works yet because I'm not aware of a
> server implementation that generates search responses for search requests=
.
> Maybe my understanding here is wrong, I asked both Guy and Brendan for
> this. Would be great to have test vectors. My implementation of a prefix
> and log tree is tested, but only "against itself," i.e., I check that my
> implementation satisfies certain invariants.
>
> We also prove that our go implementation is memory safe. We haven't gone
> much further than that in our mechanized proofs because I would first lik=
e
> to test whether the client implementation actually works. It is much
> cheaper to test than to prove, so I want to do that first.
>
> The asterisk that I mentioned above is that I took the liberty to change
> the server response format slightly so that proofs are easier to parse. I
> could, at the meeting, present my experience implementing the client. My
> life would be much simpler if the change in wire format were part of the
> draft, and I find there are certain parts of the draft which are hard to
> implement and get right.
>
> Best,
> Felix
>
>
> Am Di., 14. Juli 2026 um 16:50 Uhr schrieb Prachi Jain <
> prachi.jain1288@gmail.com>:
>
>> Hello KEYTRANS enthusiasts,
>>
>> Please share any topics, discussion items, or anything else you'd like t=
o
>> cover during our time at IETF 126. We have an hour allocated to us.
>>
>>
>> -Chairs
>> --
>> Keytrans mailing list -- keytrans@ietf.org
>> To unsubscribe send an email to keytrans-leave@ietf.org
>>
>

--000000000000a9f5120656badac0
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Thanks for sharing this, Felix. We will put you on the age=
nda.</div><br><div class=3D"gmail_quote gmail_quote_container"><div dir=3D"=
ltr" class=3D"gmail_attr">On Thu, Jul 16, 2026 at 3:14=E2=80=AFAM Felix Lin=
ker &lt;<a href=3D"mailto:linkerfelix@gmail.com">linkerfelix@gmail.com</a>&=
gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0=
px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div =
dir=3D"ltr">Hi Prachi and fellow keytrans enthusiasts,<div><br></div><div>W=
e made progress implementing a client. The client is still very much WIP, b=
ut I believe (with an asterisk) that it should be able to verify greatest v=
ersion queries.</div><div><br></div><div>The code for that can be found her=
e:=C2=A0<a href=3D"https://github.com/felixlinker/keytrans-verification/blo=
b/felixlinker/client-state/pkg/client/client.go#L98" target=3D"_blank">http=
s://github.com/felixlinker/keytrans-verification/blob/felixlinker/client-st=
ate/pkg/client/client.go#L98</a> Development currently happens on that bran=
ch.</div><div><br></div><div>I could not test whether the client works yet =
because I&#39;m not aware of a server implementation that generates search =
responses for search requests. Maybe my understanding here is wrong, I aske=
d both Guy and Brendan for this. Would be great to have test vectors. My im=
plementation of a prefix and log tree is tested, but only &quot;against its=
elf,&quot; i.e., I check that my implementation satisfies certain invariant=
s.</div><div><br></div><div>We also prove that our go implementation is mem=
ory safe. We haven&#39;t gone much further than that in our mechanized proo=
fs because I would first like to test whether the client implementation act=
ually works. It is much cheaper to test than to prove, so I want to do that=
 first.</div><div><br></div><div>The asterisk that I mentioned above is tha=
t I took the liberty to change the server response format slightly so that =
proofs are easier to parse. I could, at the meeting, present my experience =
implementing the client. My life would be much simpler if the change in wir=
e format were part of the draft, and I find there are certain parts of the =
draft which are hard to implement and get right.</div><div><br></div><div>B=
est,</div><div>Felix</div><div><br></div></div><br><div class=3D"gmail_quot=
e"><div dir=3D"ltr" class=3D"gmail_attr">Am Di., 14. Juli 2026 um 16:50=C2=
=A0Uhr schrieb Prachi Jain &lt;<a href=3D"mailto:prachi.jain1288@gmail.com"=
 target=3D"_blank">prachi.jain1288@gmail.com</a>&gt;:<br></div><blockquote =
class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px sol=
id rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr">Hello KEYTRANS enthu=
siasts,=C2=A0<div><br><div></div><div>


<p style=3D"margin:0px;font-style:normal;font-variant:normal;font-size-adju=
st:none;font-kerning:auto;font-feature-settings:normal;font-stretch:normal;=
line-height:normal;font-family:&quot;Helvetica Neue&quot;">Please share any=
 topics, discussion items, or anything else you&#39;d like to cover during =
our time at IETF 126. We have an hour allocated to us.=C2=A0</p><p style=3D=
"margin:0px;font-style:normal;font-variant:normal;font-size-adjust:none;fon=
t-kerning:auto;font-feature-settings:normal;font-stretch:normal;line-height=
:normal;font-family:&quot;Helvetica Neue&quot;"><br></p><p style=3D"margin:=
0px;font-style:normal;font-variant:normal;font-size-adjust:none;font-kernin=
g:auto;font-feature-settings:normal;font-stretch:normal;line-height:normal;=
font-family:&quot;Helvetica Neue&quot;">-Chairs</p></div></div></div>
-- <br>
Keytrans mailing list -- <a href=3D"mailto:keytrans@ietf.org" target=3D"_bl=
ank">keytrans@ietf.org</a><br>
To unsubscribe send an email to <a href=3D"mailto:keytrans-leave@ietf.org" =
target=3D"_blank">keytrans-leave@ietf.org</a><br>
</blockquote></div>
</blockquote></div>

--000000000000a9f5120656badac0--