Skip to content

Conversation

@javierdiaz72
Copy link
Contributor

This PR resolves #1569.

@javierdiaz72 javierdiaz72 self-assigned this Jul 8, 2025
@javierdiaz72 javierdiaz72 added enhancement New feature or request formal-spec Changes related to formal specifications conformance Changes related to conformance testing labels Jul 8, 2025
@dnadales dnadales moved this to 👀 In review in Consensus Team Backlog Jul 9, 2025
@javierdiaz72 javierdiaz72 marked this pull request as ready for review August 19, 2025 14:17
@javierdiaz72
Copy link
Contributor Author

Hi, team! I've just made this PR ready for review. Please note that the issue with the CI is still pending.

Copy link
Contributor

@nfrisby nfrisby left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

None of the diff has a surprising "shape", for what this PR is doing. I pointed out a few places where a comment would have helped or the existing comments didn't help me.

However, I'm only Commenting and not Approving because I didn't check the logic exhaustively. My assumption is that this is all working towards conformance testing and that---since everything has the right shape---executing the conformance tests will reveal the bugs here I might have overlooked.

If @javierdiaz72 agrees with that level of scrutiny, then I can upgrade my review to an Approval. Or else we can wait for additional scrutiny of that stuff.

, ocΣ = ocΣ'
}
where
encodedOc = 0 -- since encode (ocVkₕ , ocN , ocC₀) == 0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know where this came from encode (ocVkₕ , ocN , ocC₀) == 0, and it seems unexpected, so the comment is causing more questions than answers :D

Maybe a link/pointer to where I could understand why that triplet serializes to 0?

... aha, I grepped for encode and I see that the encoding is all still mocked with const 0. So maybe just add "due to mock serialization" to your code comment for now.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Addressed in 85065c2, please check.

-- NOTE: Why should this test succeed? Here's the explanation:
--
-- hk = hash bhbIssuerVk = hash 456 = 457
-- hk = hash bhbIssuerVk = succ bhbIssuerVk
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You lost me at hash x = succ x.

Is that a common idiom when modeling hash functions?

Copy link
Contributor Author

@javierdiaz72 javierdiaz72 Sep 29, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mock hashing is just the successor function, I'll add "due to mock hashing" to avoid confusion.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Addressed in 85065c2, please check.

sampleSignKey = skeyDSIGNToInteger $ genKeyDSIGN @Ed25519DSIGN (mkSeedFromBytes $ BC.pack $ replicate 32 '0')
extSignKES' skf n ser =
sigKESToInteger $
KES.unsoundPureSignKES
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"Unsound" is a scary word. So I looked it up: https://github.com/IntersectMBO/cardano-base/blob/5c18017546dc1032e76a985c45fe7c3df2a76616/cardano-crypto-class/src/Cardano/Crypto/KES/Class.hs#L58

It's "unsound" merely because it doesn't use mlocked memory. So it's not a concern here, since this is only for conformance testing.

A little comment here with a link and one sentence summary might be nice.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Addressed in 85065c2, please check.

, bhSig = bhSig'
}
where
encodedBhb = 0 -- since encode bhb = 0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See my other comment about "since encode foobar = 0"

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe even just since for now encode bnb = encode _ = 0 would have been enough to not incur these comments from me :D

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Addressed in 85065c2, please check.

@amesgen
Copy link
Member

amesgen commented Sep 29, 2025

Hi, team! I've just made this PR ready for review. Please note that the issue with the CI is still pending.

I opened #1697 for that, someone will address it soon 👍

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

conformance Changes related to conformance testing enhancement New feature or request formal-spec Changes related to formal specifications

Projects

Status: 👀 In review

Development

Successfully merging this pull request may close these issues.

Use the real crypto in formal spec tests

3 participants