aes-gcm: fix decryption bug, add properties #46 #75

marsella · 2024-06-12T13:19:48Z

Closes #46. Closes #74. Closes #47.

Here's an update to the AES-GCM spec that fixes the decryption bug (decryption was just implemented incorrectly, and it was never tested / proven to work anyway).
The existing version of AES is based on what I think is a submission document for the GCM algorithm. The format, algorithm names, and parameter names were changed at some point, and the official NIST standard uses some slightly different notation. I kept the old APIs in because it seems like they're being used, but changed the references and everything else to adhere to the NIST spec.

Conveniently, there were several correct implementations floating around:

In the original issue, folks proposed and implemented (Fix error in GCM decryption #47) adding a flag to this version to make decryption correct
Also in the original issue, someone provided a different implementation that more closely adheres to the AES-GCM NIST spec. This forms the basis of most of the changes in this PR.

This PR:

fixes the spec to be correct
update the properties to validate decryption (to some degree, see following questions)
adds a NIST-adherent API and states an equivalence property to the existing API
adds a basic encryption / decryption is symmetric property
adds a batch file to prove the test vectors and check the new and existing properties. I have not actually proven any of the properties that are currently :checked in the file; I added docs with a note of how long I waited.

This is now ready for review!

These questions have been answered:

The version from weaversa had a requirement that P, IV, and A are all finite. Is that redundant if we have size upper bounds on each of them? Does it still allow negative infinity? Is the fact that it's used as a length enforce that it's non-negative?
Style question: Taking / returning a named record vs a set of parameters. Why would we do one vs the other?
How can we make two type variables and constraint them to be the same, so that things look more like the human spec? (P = len_C)
Guidelines on when to use module-level parameters vs function-level?
How do I go about doing something useful with the equivalence properties in gcm.cry? Should I prove these in the batch file for some typical parameter sets? Is there a way to say for all?

I want to look into the following items:

I think the set of acceptable tag lengths is informed by the other parameters, or there might be acceptable sets in general and it should disallow other kinds (beyond just the individual length requirements). See if this is true and if we can enforce it
GHASH. Check if 128 is correct fixed size for hash or if that should be a parameter as well
I think there are additional properties that we could demo here as well, like wrong tag => invalid decryption (statistically at least)

- Adds APIs to match the NIST spec - Adds properties of API equivalence - Adds properties that test decryption bug - Adds a batch file

RyanGlScott

The version from weaversa had a requirement that P, IV, and A are all finite. Is that redundant if we have size upper bounds on each of them?

I assume you mean bounds like P <= 2^^39 - 256? If so, then yes, that implies fin P, so it would be redundant to say (fin P, P <= 2^^39 - 256).

Does it still allow negative infinity? Is the fact that it's used as a length enforce that it's non-negative?

All type-level numbers are non-negative, so you don't need to worry about negative infinity.

Style question: Taking / returning a named record vs a set of parameters. Why would we do one vs the other?

This is ultimately a matter of taste, so there aren't any hard guidelines. That being said, I think that if you start using tuples that are sufficiently large (say, four or more elements), then I would generally prefer using records at that point. Naming the fields makes it easier to tell at a glance what each field represents, and it confers the advantage that you can construct the record without needing to remember the exact order in which the fields were defined.

How can we make two type variables and constraint them to be the same, so that things look more like the human spec? (P = len_C)

I'm not quite sure what you mean here. Can you give an example of what you are trying to do?

Guidelines on when to use module-level parameters vs function-level?

In general, you'd make something a module-level parameter if it is shared among multiple functions in the module (e.g., the key size K). Again, I think this comes down to a matter of taste.

How do I go about doing something useful with the equivalence properties in gcm.cry? Should I prove these in the batch file for some typical parameter sets? Is there a way to say for all?

You could try :check'ing some of the properties. For certain properties, you might even be able to cover all possible inputs using :prove, but I imagine that some properties will simply be too complicated to :prove in a reasonable amount of time (this is where you'd need SAW to do better). But even just :check would be better than nothing.

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

- switches from gross coerceSize function to nice numeric constraints - removes Option due to limited SAW support - adjusts some naming to more closely match spec

marsella · 2024-06-14T14:01:16Z

How can we make two type variables and constraint them to be the same, so that things look more like the human spec? (P = len_C)

I'm not quite sure what you mean here. Can you give an example of what you are trying to do?

I was missing the type keyword. The method uses parameter P to define the length of the plaintext and ciphertext, while the NIST spec uses len(C). I was trying to figure out how to add a variable called len_C to use in different operations that had the same value as P, but I was trying to do it value-wise (len_C ='P) when I should've been defining a type variable (type len_C = P).

marsella · 2024-06-17T13:02:26Z

Here are some follow-up notes:

The parameter choices in the implementation are a bit looser than what's described in the spec. Specifically:
- P17: t may be any one of the following five values: 128, 120, 112, 104, or 96
- P15: the block size shall be 128 bits
- P15: the key size shall be at least 128 bits
- P16: len(P) $\le 2^{39}-256$; len(P) is a multiple of 8
- P16: len(A) $\le 2^{64}-1$; len(A) is a multiple of 8
- P16: $1 \le \text{len(IV)} \le 2^64-1$; len(IV) is a multiple of 8
- encrypt and decrypt have to support the same len(C, A, IV)s.
Parameter architecture: I looked at AES_parameterized but it looks to be more flexible than the actual set of NIST-approved parameters (FIPS 197, update 1). The expected parameters are encoded in AES.cry so I don't understand what the parameterized version is doing. ValidKey constraint seems too flexible; doesn't it have to be exactly the expected key length?
- Maybe this is what Joe was mentioning about parameterizations; currently you have to manually change the line in AES.cry to change between parameter sets, but it would be nicer to just define the 3 sets and be done.
The GHASH signature is correct.
Properties: there are some additional properties we could prove here. Initial thoughts:
- Do we write negative tests? I added one property that asserts that the wrong tag will fail, but that's not super compelling.
- We could try proving symmetry dec (enc x) = x. If we did so, I'd like to pick the most-common parameter sets used in the wild (plaintext and aad length are kind of a wildcard here but key / IV / tag length likely have only a few common configs used in practice).
- I don't think this GCM is used for any other block ciphers, but if it was we could test them
- Lots of tests are commented out in AES.cry
- GCTR: if X is empty, return Y = empty string. This is obvious from observation but we could still test it
  - related: do we write properties for private functions? Do those just live outside the private block even though nobody would use them outside the batch file?
- Cryptol is not suited to proving properties over time, right? As in, the IV is a nonce and must be chosen uniquely across different encryptions, but there's no way to specify that in the AE function.

RyanGlScott · 2024-06-17T13:22:17Z

I've attempted to answer the questions that I feel qualified to answer:

Do we write negative tests? I added one property that asserts that the wrong tag will fail, but that's not super compelling.

I am generally a fan of more tests, although I don't have a suggestion for how to make it more compelling than what you currently have.

We could try proving symmetry dec (enc x) = x.

Yes, I agree that that is a pretty compelling property to test, even if we only test it on specific inputs.

Lots of tests are commented out in AES.cry

I can provide at least a partial explanation for this, since I recently modified the code in AES.cry. In 0a60f79, the key size for AES was changed from 128 bits to 256 bits. Before that change, only the 128-bit tests were used, and tests written with other key sizes in mind were commented out. To keep the existing convention, that commit comments out the 128-bit tests and enables the 256-bit tests.

We could, in principle, enable the tests at other key sizes as well, but I think we'd need to parameterize the code in AES.cry more in order to make this possible, as everything in AES.cry currently assumes 256-bit key sizes. (Whether this level of parameterization is desired or not is unclear to me.)

GCTR: if X is empty, return Y = empty string. This is obvious from observation but we could still test it

Yes, we may as well test this.

related: do we write properties for private functions? Do those just live outside the private block even though nobody would use them outside the batch file?

We can certainly test properties over private functions. Note that Cryptol doesn't yet have a clean way to mark properties as private (see GaloisInc/cryptol#1621), but that needn't be a blocker.

Cryptol is not suited to proving properties over time, right? As in, the IV is a nonce and must be chosen uniquely across different encryptions, but there's no way to specify that in the AE function.

I don't think there is any direct way to prove that, other than perhaps checking if the particular values of IV at specific instantiations of AES-GCM are distinct.

marsella · 2024-06-17T16:13:34Z

Thank you! Appreciate the context on the AES parameterization.

I think there's a more general question here about whether we want to support smaller AES key sizes and if so, whether we're satisfied with the given structure -- 128 is mostly not recommended in practice but it's still part of Suite B so we might want to have easier access to it. I was looking at the Kyber implementation which is generic over parameters and then has a few modules that just define the standardized parameter sets. This is definitely out of scope for this PR but we might consider it if we come at this piece in the future.

Cryptol is not suited to proving properties over time, right? As in, the IV is a nonce and must be chosen uniquely across different encryptions, but there's no way to specify that in the AE function.

I don't think there is any direct way to prove that, other than perhaps checking if the particular values of IV at specific instantiations of AES-GCM are distinct.

I was wondering more if there's a way to say, like, a type is a 128-bit string drawn uniformly at random but that seems very hard to mechanically reason about.

- separates private methods in GCM module - tries to make naming more canonical across properties - adds additional properties for AES-GCM - expands batch file and documentation for AES-GCM

marsella

This is now ready for review!

I welcome nit-picky feedback on naming, spacing, and style from those who are more familiar with Cryptol standards than I am (e.g. everyone here).

Should I try to prove the 'check`ed properties before merging this? Do we have a standard setup on an external machine for doing so or would I just let it run overnight on my laptop?

Before I merge this I am going to make a separate issue collecting the concerns I noted in a previous comment so they don't get lost.

marsella · 2024-06-17T18:30:05Z

Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat

+:check decryptionApisAreEquivalent `{K=128, IV=96, AAD=0, T=128, P=256} {E=AES::encrypt}
+:check encryptionApisAreEquivalent `{K=128, IV=96, AAD=0, T=128, P=256} {E=AES::encrypt}


style question: Should I parameterize these in the AES-GCM module with AES so we don't have to do it manually here? I did that for aesGcmIsSymmetric

Sure, that seems reasonable.

marsella · 2024-06-17T18:31:27Z

Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat

+// This property is independent of the type parameters but we have to specify
+// them anyway.
+// It takes more than 25 minutes to prove.
+:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt}


note: None of these parameters are relevant because this is just a function on 128-bit blocks. Should I make a separate batch file for it? Is there a way to reorganize the GCM module so that this property and the two relevant functions are not bound by the module parameters?

We could imagine splitting up the module hierarchy more to make dotAndMultAreEquivalent only parameterized over K. That being said, it's unclear that doing so would pay its weight. Personally, I think it's fine to just invoke dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} like you do here.

marsella · 2024-06-17T18:32:52Z

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

+      // Set names to match the spec
+      type s = len_IV %^ 128  // Equivalently: 128 * len_IV /^ 128 - len_IV
+
+  /**


Note: everything from here down, as well as most of the GCM_AE and GCM_AD methods are pulled from the implementation @weaversa provided in #46. Do we have a standard way of citing this? Does cryptol-specs try to maintain the authorship notes at the top of the file?

I think it would be nice to credit Sean in the copyright info above.

Agreed on this comment.

marsella · 2024-06-17T18:38:50Z

Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry


+property AES_GCM_invalid_test_vector =


note: This is just a single negative test made by borking the tag from the fourth test vector. It's not exactly superseded by the symmetric property because that doesn't guarantee that there's only one correct tag for a given (key, iv, ct) tuple. I'm going to make a note of this in the subsequent clean-up issue.

marsella

@mccleeary-galois We talked a few days ago about proving properties that I thought would be fast but were not actually fast in practice. Not sure how much of a priority it is to dive into the SMT statements for these, but I'll tag them below for ya.

marsella · 2024-06-20T13:34:00Z

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

+/**
+* Property demonstrating equivalence between `gcmDec` and `GCM_AD`.
+*/
+decryptionApisAreEquivalent : {P} ( fin P, P <= 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> [T] -> Bool
+property decryptionApisAreEquivalent key iv ct aad tag =
+      gcmDec { key=key, iv=iv, ct=ct, aad=aad, tag=tag}
+      == GCM_AD key iv ct aad tag

+/**
+ * Property demonstrating equivalence between `gcmEnc` and `GCM_AE`.
+ */
+encryptionApisAreEquivalent : {P} ( fin P, P <= 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> Bool
+property encryptionApisAreEquivalent key iv pt aad = gcm_ae_output == (gcmEnc_output.ct, gcmEnc_output.tag)
+    where
+      input = { key=key, iv=iv, pt=pt, aad=aad }
+      gcmEnc_output = gcmEnc input
+      gcm_ae_output = GCM_AE key iv pt aad


Here are the definitions of the equivalence properties. They're parameterized and called in the batch file.

I expected these to be fast to prove because gcmEnc calls GCM_AE, but they are not.

How long are these proofs taking at the moment?

I have not run them to completion, but more than 25 minutes. I can set them spinning on my laptop and see if they end by the end of the day.

marsella · 2024-06-20T13:36:57Z

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

+gcmIsSymmetric : {P} ( fin P, P < 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> Bool
+property gcmIsSymmetric key iv pt aad = dec.valid && (dec.pt == pt)
+    where
+        (ct, tag) = GCM_AE key iv pt aad
+        dec = GCM_AD key iv ct aad tag


Here's the symmetric property. It's parameterized in AES_GCM.cry and called in the batch file. I expected this to be fast-ish to prove because most of the steps of GCM-AE are duplicated in GCM-AD but it is not.

I think we should settle for a :check in the batch file at the moment.

RyanGlScott · 2024-06-20T14:11:44Z

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

+      // Set names to match the spec
+      type s = len_IV %^ 128  // Equivalently: 128 * len_IV /^ 128 - len_IV
+
+  /**


I think it would be nice to credit Sean in the copyright info above.

RyanGlScott · 2024-06-20T14:17:47Z

Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat

+
+// This property is independent of the type parameters but we have to specify
+// them anyway.
+// It takes more than 25 minutes to prove.


Do you have a sense for what is causing it to be so slow?

In any case, it may be wise to reduce the number of random tests that we do in Cryptol to make this complete in a more reasonable amount of time. You can do this in a Cryptol batch file by running:

:set tests=<N>

The default value of <N> is 100, so we could certainly stand to lower it if these tests take an excessively long time to complete.

Oh, this isn't clear. The :check here is fairly fast, but calling it with :prove instead is very slow. I think if we want to claim that this is formally verified we'd need to eventually :prove it. I don't know why :prove is so slow, but I have no intuition for how Cryptol works or how to form properties that might prove faster or slower.

My apologies, I interpreted the comment above as applying to :check rather than :prove. In that case, the call to :check here is fine as-is. (I am not surprised that it takes so long to prove, for reasons mentioned in #75 (comment).)

RyanGlScott · 2024-06-20T14:21:37Z

Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat

+// This property is independent of the type parameters but we have to specify
+// them anyway.
+// It takes more than 25 minutes to prove.
+:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt}


We could imagine splitting up the module hierarchy more to make dotAndMultAreEquivalent only parameterized over K. That being said, it's unclear that doing so would pay its weight. Personally, I think it's fine to just invoke dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} like you do here.

RyanGlScott · 2024-06-20T14:22:20Z

Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat

+:check decryptionApisAreEquivalent `{K=128, IV=96, AAD=0, T=128, P=256} {E=AES::encrypt}
+:check encryptionApisAreEquivalent `{K=128, IV=96, AAD=0, T=128, P=256} {E=AES::encrypt}


Sure, that seems reasonable.

RyanGlScott · 2024-06-20T14:26:58Z

Should I try to prove the 'check`ed properties before merging this?

You can certainly try, but I wouldn't invest too much time in doing so. We've had to spend a considerable amount of effort to prove similar properties about AES-GCM in SAW, and this required manually rewriting proof goals. I would be very surprised if Cryptol could prove properties of a similar level of complexity without any assistance from a proof engineer.

mccleeary-galois · 2024-06-21T14:34:17Z

Should I try to prove the 'check`ed properties before merging this?

You can certainly try, but I wouldn't invest too much time in doing so. We've had to spend a considerable amount of effort to prove similar properties about AES-GCM in SAW, and this required manually rewriting proof goals. I would be very surprised if Cryptol could prove properties of a similar level of complexity without any assistance from a proof engineer.

Agreed with @RyanGlScott here, I took a peak at this a bit and it would almost certainly require some proof engineering... I think leaving things as :check is good enough for now.

mccleeary-galois · 2024-06-21T14:41:18Z

This is a great step in the right direction for this! Generally LGTM for what the scope of this ticket is.
Most of my comments are around future concerns of CI automation.

mccleeary-galois · 2024-06-21T14:32:11Z

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

+      // Set names to match the spec
+      type s = len_IV %^ 128  // Equivalently: 128 * len_IV /^ 128 - len_IV
+
+  /**


Agreed on this comment.

mccleeary-galois · 2024-06-21T14:35:41Z

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

+/**
+* Property demonstrating equivalence between `gcmDec` and `GCM_AD`.
+*/
+decryptionApisAreEquivalent : {P} ( fin P, P <= 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> [T] -> Bool
+property decryptionApisAreEquivalent key iv ct aad tag =
+      gcmDec { key=key, iv=iv, ct=ct, aad=aad, tag=tag}
+      == GCM_AD key iv ct aad tag

+/**
+ * Property demonstrating equivalence between `gcmEnc` and `GCM_AE`.
+ */
+encryptionApisAreEquivalent : {P} ( fin P, P <= 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> Bool
+property encryptionApisAreEquivalent key iv pt aad = gcm_ae_output == (gcmEnc_output.ct, gcmEnc_output.tag)
+    where
+      input = { key=key, iv=iv, pt=pt, aad=aad }
+      gcmEnc_output = gcmEnc input
+      gcm_ae_output = GCM_AE key iv pt aad


How long are these proofs taking at the moment?

mccleeary-galois · 2024-06-21T14:40:21Z

Primitive/Symmetric/Cipher/Authenticated/GCM.cry

+gcmIsSymmetric : {P} ( fin P, P < 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> Bool
+property gcmIsSymmetric key iv pt aad = dec.valid && (dec.pt == pt)
+    where
+        (ct, tag) = GCM_AE key iv pt aad
+        dec = GCM_AD key iv ct aad tag


I think we should settle for a :check in the batch file at the moment.

- improves some documentation - moves parameterization of several properties into the aes-gcm module, instead of doing it on the fly in the batch file

marsella · 2024-06-21T18:21:00Z

I made #77 and #78 to collect some of the other concerns raised here.

aes-gcm: fix decryption bug, add properties #46

bea3dc8

- Adds APIs to match the NIST spec - Adds properties of API equivalence - Adds properties that test decryption bug - Adds a batch file

RyanGlScott reviewed Jun 12, 2024

View reviewed changes

Primitive/Symmetric/Cipher/Authenticated/GCM.cry Outdated Show resolved Hide resolved

Primitive/Symmetric/Cipher/Authenticated/GCM.cry Outdated Show resolved Hide resolved

aes-gcm: improve types in API #46

fad9368

- switches from gross coerceSize function to nice numeric constraints - removes Option due to limited SAW support - adjusts some naming to more closely match spec

aes-gcm: clean up GCM and AES-GCM modules

1b91298

- separates private methods in GCM module - tries to make naming more canonical across properties - adds additional properties for AES-GCM - expands batch file and documentation for AES-GCM

marsella commented Jun 17, 2024

View reviewed changes

marsella marked this pull request as ready for review June 17, 2024 18:47

marsella commented Jun 20, 2024

View reviewed changes

RyanGlScott reviewed Jun 20, 2024

View reviewed changes

mccleeary-galois self-requested a review June 21, 2024 14:41

mccleeary-galois approved these changes Jun 21, 2024

View reviewed changes

aes-gcm: clarify documentation, properties #46

4dec0e6

- improves some documentation - moves parameterization of several properties into the aes-gcm module, instead of doing it on the fly in the batch file

marsella merged commit 1e31efb into master Jun 21, 2024

marsella deleted the 46-fix-aes-bug branch June 21, 2024 17:57

This was referenced Jun 21, 2024

Fix error in GCM decryption #47

Closed

Update AES-GCM to meet "gold standard" requirements #78

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

aes-gcm: fix decryption bug, add properties #46 #75

aes-gcm: fix decryption bug, add properties #46 #75

marsella commented Jun 12, 2024 •

edited

Loading

RyanGlScott left a comment

marsella commented Jun 14, 2024 •

edited

Loading

marsella commented Jun 17, 2024 •

edited

Loading

RyanGlScott commented Jun 17, 2024

marsella commented Jun 17, 2024 •

edited

Loading

marsella left a comment •

edited

Loading

marsella Jun 17, 2024

RyanGlScott Jun 20, 2024

marsella Jun 17, 2024

RyanGlScott Jun 20, 2024 •

edited

Loading

marsella Jun 17, 2024

RyanGlScott Jun 20, 2024

mccleeary-galois Jun 21, 2024

marsella Jun 17, 2024

marsella left a comment

marsella Jun 20, 2024

mccleeary-galois Jun 21, 2024

marsella Jun 21, 2024

marsella Jun 20, 2024

mccleeary-galois Jun 21, 2024

RyanGlScott Jun 20, 2024

RyanGlScott Jun 20, 2024

marsella Jun 20, 2024

RyanGlScott Jun 20, 2024

RyanGlScott Jun 20, 2024 •

edited

Loading

RyanGlScott Jun 20, 2024

RyanGlScott commented Jun 20, 2024

mccleeary-galois commented Jun 21, 2024

mccleeary-galois commented Jun 21, 2024

mccleeary-galois Jun 21, 2024

mccleeary-galois Jun 21, 2024

mccleeary-galois Jun 21, 2024

marsella commented Jun 21, 2024

		:check decryptionApisAreEquivalent `{K=128, IV=96, AAD=0, T=128, P=256} {E=AES::encrypt}
		:check encryptionApisAreEquivalent `{K=128, IV=96, AAD=0, T=128, P=256} {E=AES::encrypt}

aes-gcm: fix decryption bug, add properties #46 #75

aes-gcm: fix decryption bug, add properties #46 #75

Conversation

marsella commented Jun 12, 2024 • edited Loading

This is now ready for review!

RyanGlScott left a comment

Choose a reason for hiding this comment

marsella commented Jun 14, 2024 • edited Loading

marsella commented Jun 17, 2024 • edited Loading

RyanGlScott commented Jun 17, 2024

marsella commented Jun 17, 2024 • edited Loading

marsella left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RyanGlScott Jun 20, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

marsella left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RyanGlScott Jun 20, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RyanGlScott commented Jun 20, 2024

mccleeary-galois commented Jun 21, 2024

mccleeary-galois commented Jun 21, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

marsella commented Jun 21, 2024

marsella commented Jun 12, 2024 •

edited

Loading

marsella commented Jun 14, 2024 •

edited

Loading

marsella commented Jun 17, 2024 •

edited

Loading

marsella commented Jun 17, 2024 •

edited

Loading

marsella left a comment •

edited

Loading

RyanGlScott Jun 20, 2024 •

edited

Loading

RyanGlScott Jun 20, 2024 •

edited

Loading