Ns/chore/encode a tilde

[nsarlin-zama]

closes: please link all relevant issues

PR content/description

Fix the hashed statement to match the reference paper:

• hash a more flexible representation of \tilde{A}: the matrix is represented using:
  • a bit vector representing the position of the bits that are proven to be 0. This vector will be derived from the number of msb bits proven to be 0
  • a and b, the public key
• hash the bound on the infinite norm instead of the squared bound on the euclidean norm
• hash k (number of slots)

For backward compat, these options are part of a HashConfig object. However, this object cannot be constructed from tfhe-rs. That way, we know that the only possible config are the ones that have been defined as default at some point.

---

This change is 

[IceTDrinker]

I see you went for a fully modular approach for the update but I think I wuold prefer if we forced proofs to be either the way they were before or the fixed way, not a mix of all possibilities, because it makes it harder to test and to defend against bad configs, so we would have a sort of V2_0 and then a V2_1 ? wdyt ?

@IceTDrinker reviewed 11 of 14 files at r1, all commit messages.
Reviewable status: 11 of 14 files reviewed, 3 unresolved discussions (waiting on @mayeul-zama and @tmontaigu)

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 85 at r1 (raw file):

#[derive(Debug, Clone, Copy, Serialize, Deserialize, Versionize)]
#[versionize(PkeV2HashConfigVersions)]
pub struct PkeV2HashConfig {

while it's a nice effort, I don't think we want that much flexibility ?

---

utils/tfhe-backward-compat-data/crates/generate_1_5/src/lib.rs line 39 at r1 (raw file):

// We have a proven list generated for 0.11, but since this version the hash modes have evolved so
// we re generate one

do the zk backward tests verify the proof ?

---

tfhe/src/integer/ciphertext/compact_list.rs line 1165 at r1 (raw file):

    pub fn forbid_proven_zero_bits_encoding(
        self,
        forbidden_proven_zero_bits_encoding: ZkPkeV2ProvenZeroBitsEncoding,

feels like too many options don't you think ? could this be handled all at once instead of for each parameter ? I haven't read the rest of the zk code but it feels like this gives too much control on the settings (maybe Im wrong)

[nsarlin-zama]

Reworked, I kept the struct for internal use but only a limited set of possibility is now exposed.

Reviewable status: 6 of 14 files reviewed, 3 unresolved discussions (waiting on @IceTDrinker, @mayeul-zama, and @tmontaigu)

---

tfhe/src/integer/ciphertext/compact_list.rs line 1165 at r1 (raw file):

Previously, IceTDrinker wrote…

feels like too many options don't you think ? could this be handled all at once instead of for each parameter ? I haven't read the rest of the zk code but it feels like this gives too much control on the settings (maybe Im wrong)

removed

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 85 at r1 (raw file):

Previously, IceTDrinker wrote…

while it's a nice effort, I don't think we want that much flexibility ?

this feels a bit clearer in the impl than having to guess what is the expected behavior based on the name. This is now not serialized anymore, only a fixed enum of possibilities is included in the proof.

---

utils/tfhe-backward-compat-data/crates/generate_1_5/src/lib.rs line 39 at r1 (raw file):

Previously, IceTDrinker wrote…

do the zk backward tests verify the proof ?

yes if this is a proven list we use verify_and_expand

[IceTDrinker]

think I'm confused by the way the encoding is built, I would have expected to have it match the layout of slots when taken in an MSB repr i.e. for 2 slots :

| = slot separation || = byte separation

01111 | 011 || 11 | xxxxxx

xxxxxx here being empty values that would be 0s, so we would have 0b01111011 and 0b11000000 but it does not seem to be the cas e?

e.g.

several comments/questions

but overall I think this is preferrable to the original version, this makes it easier to reason about the configurations that were actually implemented

@IceTDrinker reviewed 8 of 8 files at r2, all commit messages.
Reviewable status: all files reviewed, 21 unresolved discussions (waiting on @mayeul-zama and @tmontaigu)

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 44 at r2 (raw file):

#[derive(Debug, Clone, Copy)]
/// How the position of bits proven to be 0 is encoded
pub enum PkeV2ProvenZeroBitsEncoding {

likely can be pub(crate) ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 48 at r2 (raw file):

    MsbZeroBitsCountOnly = 0,
    /// Flexible encoding that allows to define any bit in any slot as being proven to be 0
    AnyBitAnySlot = 1,

is this variant ever used in the crate today ? or is it for future proofing ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 71 at r2 (raw file):

#[derive(Debug, Clone, Copy)]
/// The kind of norm bound that is hashed in the statement.
pub enum PkeV2HashedBoundType {

likely can be pub(crate) ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 75 at r2 (raw file):

    SquaredEuclideanNorm = 0,
    /// Hash the infinite norm given as input by the prover
    InfiniteNorm = 1,

InfinityNorm I think ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 79 at r2 (raw file):

#[derive(Debug, Clone, Copy)]
pub struct PkeV2HashConfig {

let's make all "internal" types for the config pub(crate) ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 113 at r2 (raw file):

    V0_4_0 = 0,
    V0_7_0 = 1,
    V0_8_0 = 2,

what's the reason for giving enum variants, integer indices explicitely ?

also I see a 0_8_0 version but I don't think you updated the cargo.toml yet, it's something that can be done in this PR

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 132 at r2 (raw file):

const PKEV2_HASH_CONFIG_V0_8_0: PkeV2HashConfig = PkeV2HashConfig {
    mode: PkeV2HashMode::Compact,
    proven_zero_bits_encoding: PkeV2ProvenZeroBitsEncoding::AnyBitAnySlot,

Is that true though ? even if the encoding supports the any bit any slot, in practice we still prove only the MSB ?

ah no ok, it's the generic new encoding but we still prove only a given number of MSB ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 134 at r2 (raw file):

    proven_zero_bits_encoding: PkeV2ProvenZeroBitsEncoding::AnyBitAnySlot,
    hashed_bound_type: PkeV2HashedBoundType::InfiniteNorm,
    hash_k: false,

the point was to have this to true I think for the updated proof ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 142 at r2 (raw file):

    // compatibility.
    fn default() -> Self {
        Self::V0_8_0

I would add a lint to make sure this version matches the one in Cargo.toml, otherwise easy to forget

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 190 at r2 (raw file):

        u64::MAX
    } else {
        !(u64::MAX << effective_t_log2)

so the t_log2 low bits have the encoding of the bits proven to be 0 or not ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 209 at r2 (raw file):

        // Dump the temporary buffer into the byte vec until there is less that a full byte left
        while bits_in_buffer >= u8::BITS {
            packed.push((bit_buffer & 0xff) as u8);

I think the masking is not useful here ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 210 at r2 (raw file):

        while bits_in_buffer >= u8::BITS {
            packed.push((bit_buffer & 0xff) as u8);
            bit_buffer >>= 8;

could still use u8::BITS here and below

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 216 at r2 (raw file):

    if bits_in_buffer > 0 {
        packed.push((bit_buffer & 0xff) as u8);

do you have a test case that makes sure this is triggered ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 399 at r2 (raw file):

            q.to_le_bytes().as_slice(),
            (d as u64).to_le_bytes().as_slice(),
            hashed_k.as_slice(),

order matching the new description ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 1387 at r2 (raw file):

        // Test the most common case
        let res = encode_proven_zero_bits_anybit_anyslot(1, 1 << 5, 6);
        // 11110 * 6

this feels reversed with what I'm used to ?

i.e. the left most bit should be the padding bit ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 1389 at r2 (raw file):

        // 11110 * 6
        // 11110|111 10|11110|1 1110|1111 0|11110
        let expected = vec![0b11101111, 0b10111101, 0b11110111, 0b11110];

feels like the last byte should have it's low bits set to 0 ?

I think we don't see the endianness in the sam way here, and I have to say the current choice does not align with our standard represententation of the discretized torus as u64 when we discuss e.g. on a board ?

---

tfhe-zk-pok/src/backward_compatibility/pke_v2.rs line 163 at r2 (raw file):

    type Error = UnsupportedHashConfig;

    fn try_from(value: PkeV2HashMode) -> Result<Self, Self::Error> {

don't know where it's defined, but if PkeV2HashMode is deprecated, let's make it pub(crate) ?

---

tfhe-zk-pok/src/backward_compatibility/pke_v2.rs line 165 at r2 (raw file):

    fn try_from(value: PkeV2HashMode) -> Result<Self, Self::Error> {
        match value {
            PkeV2HashMode::BackwardCompat => Ok(PkeV2SupportedHashConfig::V0_4_0),

does not seem to match the file tfhe/src/zk/mod.rs the way you updated the hash mode names ?

also stupid question but if PkeV2HashMode is Versionize (don't know if it's the case) why change the name of the enum ?

---

tfhe-zk-pok/src/backward_compatibility/pke_v2.rs line 167 at r2 (raw file):

            PkeV2HashMode::BackwardCompat => Ok(PkeV2SupportedHashConfig::V0_4_0),
            PkeV2HashMode::Classical => Err(UnsupportedHashConfig(String::from(
                "Proof use hash mode \"Classical\" which has never been part of a default configuration",

mus thave been in 0.6 maybe ?

just confused the mode would not have been used if an update was made in 0.7 🤔

---

tfhe-zk-pok/src/proofs/pke_v2/mod.rs line 834 at r2 (raw file):

        load,
        seed,
        PkeV2SupportedHashConfig::default(),

why default and not an explicit value ?

---

tfhe-zk-pok/src/proofs/pke_v2/mod.rs line 2709 at r2 (raw file):

                &crs,
                &seed.to_le_bytes(),
                PkeV2SupportedHashConfig::default(),

same question below for the default ? guessing to have the latest variant ? which requires making sure the enum #[default] attribute is always on the proper variant ?

[nsarlin-zama]

In this representation we have a bit string at this point that is of an arbitrary length (a multiple of the slot size but not a multiple of 8 so no padding). I represent this this way so that the order of bits in slots is the same as the order of the slots in the string.
Since the string is built on chunks of one size (the slot size) and then decomposed in chunks of another size (the size of a byte) it is easier for me to reason about it this way.

For example if we have bi for bits indices and sj for slot indices, that would give (eg 3 slots of 3 bits):

s0b0 s0b1 s0b2 s1b0 s1b1 s1b2 s2b0 s0b1 s0b2 which feels more natural than going from left to right for the slots and from right to left for the bits.

Here if the slot size is t, the value of any substring is simply ∑sjbi*2^(tj+i)

When I represent them inside a byte I use the usual notation but start the value with 0b to make it clear.

Reviewable status: all files reviewed, 21 unresolved discussions (waiting on @mayeul-zama and @tmontaigu)

[nsarlin-zama]

Reviewable status: all files reviewed, 21 unresolved discussions (waiting on @IceTDrinker, @mayeul-zama, and @tmontaigu)

---

tfhe-zk-pok/src/backward_compatibility/pke_v2.rs line 165 at r2 (raw file):

Previously, IceTDrinker wrote…

does not seem to match the file tfhe/src/zk/mod.rs the way you updated the hash mode names ?

also stupid question but if PkeV2HashMode is Versionize (don't know if it's the case) why change the name of the enum ?

Because it is not the same thing, PkeV2HashMode is just one attribute of the config. I need to keep it versionize because it was serialized in previous versions.

---

tfhe-zk-pok/src/backward_compatibility/pke_v2.rs line 167 at r2 (raw file):

Previously, IceTDrinker wrote…

mus thave been in 0.6 maybe ?

just confused the mode would not have been used if an update was made in 0.7 🤔

Classical has never been used by default, I was asked to add it for completeness.
We have used "BackwardCompat" from 0.4.0 to 0.7.0 (not included) and then Compact since 0.7.0

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 48 at r2 (raw file):

Previously, IceTDrinker wrote…

is this variant ever used in the crate today ? or is it for future proofing ?

It's the one used by default in this pr

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 79 at r2 (raw file):

Previously, IceTDrinker wrote…

let's make all "internal" types for the config pub(crate) ?

I can yes, but maybe being able to read those via a getter could be useful for debug, for example to print the values associated with a config ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 113 at r2 (raw file):

Previously, IceTDrinker wrote…

what's the reason for giving enum variants, integer indices explicitely ?

also I see a 0_8_0 version but I don't think you updated the cargo.toml yet, it's something that can be done in this PR

the explicit integer indices is because they are used in the EnumSet that allows to forbid some config. This builds a set by packing the values in a u128.

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 132 at r2 (raw file):

Previously, IceTDrinker wrote…

Is that true though ? even if the encoding supports the any bit any slot, in practice we still prove only the MSB ?

ah no ok, it's the generic new encoding but we still prove only a given number of MSB ?

yes this enum is just about the encoding. Note that all this HashConfig is just about how things are hashed (and encoded), but is not a generic Zk config.

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 134 at r2 (raw file):

Previously, IceTDrinker wrote…

the point was to have this to true I think for the updated proof ?

ah yes my bad

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 142 at r2 (raw file):

Previously, IceTDrinker wrote…

I would add a lint to make sure this version matches the one in Cargo.toml, otherwise easy to forget

Yes ideally, but I am not sure if this is easy to do ?

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 190 at r2 (raw file):

Previously, IceTDrinker wrote…

so the t_log2 low bits have the encoding of the bits proven to be 0 or not ?

if effective log t is 4, u64::MAX << effective_t_log2 is 0b111...110000 so !(u64::MAX << effective_t_log2) is 0b1111

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 209 at r2 (raw file):

Previously, IceTDrinker wrote…

I think the masking is not useful here ?

It's not, I added it for explicitness but it's a bit overkill

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 210 at r2 (raw file):

Previously, IceTDrinker wrote…

could still use u8::BITS here and below

yes

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 216 at r2 (raw file):

Previously, IceTDrinker wrote…

do you have a test case that makes sure this is triggered ?

yes I think both testcases should trigger this

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 399 at r2 (raw file):

Previously, IceTDrinker wrote…

order matching the new description ?

yes

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 1389 at r2 (raw file):

Previously, IceTDrinker wrote…

feels like the last byte should have it's low bits set to 0 ?

I think we don't see the endianness in the sam way here, and I have to say the current choice does not align with our standard represententation of the discretized torus as u64 when we discuss e.g. on a board ?

I don't understand the first question, the lsb is 0 here ?

For the other question see my answer above

---

tfhe-zk-pok/src/proofs/pke_v2/mod.rs line 834 at r2 (raw file):

Previously, IceTDrinker wrote…

why default and not an explicit value ?

Because that way we only have a single place to change the value. The prod config and the extensive tests use the default so we know that there are always in sync. There is a test for the backward compat where we set the tested versions.

---

tfhe-zk-pok/src/proofs/pke_v2/mod.rs line 2709 at r2 (raw file):

Previously, IceTDrinker wrote…

same question below for the default ? guessing to have the latest variant ? which requires making sure the enum #[default] attribute is always on the proper variant ?

this is a manual implementation. For me this is what defaults are for, user code (even in the same crate) shouldn't have to worry about which version is the one to use unless they have specific needs (such as tests of legacy configs).

[nsarlin-zama]

I detailed a bit more the comments about the packing algo

Reviewable status: 13 of 14 files reviewed, 21 unresolved discussions (waiting on @IceTDrinker, @mayeul-zama, and @tmontaigu)

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 75 at r2 (raw file):

Previously, IceTDrinker wrote…

InfinityNorm I think ?

fixed

[IceTDrinker]

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 142 at r2 (raw file):

Previously, nsarlin-zama (Nicolas Sarlin) wrote…

Yes ideally, but I am not sure if this is easy to do ?

prefer #[default] in the enum definition maybe ?

[nsarlin-zama]

Reviewable status: 11 of 14 files reviewed, 20 unresolved discussions (waiting on @IceTDrinker, @mayeul-zama, and @tmontaigu)

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 142 at r2 (raw file):

Previously, IceTDrinker wrote…

prefer #[default] in the enum definition maybe ?

done

[nsarlin-zama]

Added a new commit for supports of #[default] in types that derive Versionize

Reviewable status: 11 of 16 files reviewed, 20 unresolved discussions (waiting on @IceTDrinker, @mayeul-zama, and @tmontaigu)

[nsarlin-zama]

bumped versions of versionable and zk-pok

[IceTDrinker]

@IceTDrinker reviewed 2 of 2 files at r4, 1 of 1 files at r5, 2 of 2 files at r6, 4 of 4 files at r7, all commit messages.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @IceTDrinker, @mayeul-zama, and @tmontaigu)

---

utils/tfhe-versionable-derive/src/versionize_attribute.rs line 23 at r7 (raw file):

/// should be propagated to the newly created type.
pub(crate) const PRESERVED_FIELD_ATTRIBUTE_NAMES: [&str; 9] = [
    "serde",

as discussed let's do a quick review of what seems to make sense here + a comment to explain the rationale to propagate a given attribute/family of attibutes

[nsarlin-zama]

Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @mayeul-zama and @tmontaigu)

---

utils/tfhe-versionable-derive/src/versionize_attribute.rs line 23 at r7 (raw file):

Previously, IceTDrinker wrote…

as discussed let's do a quick review of what seems to make sense here + a comment to explain the rationale to propagate a given attribute/family of attibutes

done

[IceTDrinker]

to check the CI would have failed

@IceTDrinker reviewed 1 of 1 files at r9, all commit messages.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @IceTDrinker, @mayeul-zama, and @tmontaigu)

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 396 at r9 (raw file):

        let hashed_k = if config.hash_k {
            k.to_le_bytes().to_vec()

needs to have a fixed len type for the hashes otherwise, I'll approve to check our CI would have caught it

[nsarlin-zama]

caught by ci: https://github.com/zama-ai/tfhe-rs/actions/runs/18937136459/job/54066812914?pr=2950

Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @IceTDrinker, @mayeul-zama, and @tmontaigu)

---

tfhe-zk-pok/src/proofs/pke_v2/hashes.rs line 396 at r9 (raw file):

Previously, IceTDrinker wrote…

needs to have a fixed len type for the hashes otherwise, I'll approve to check our CI would have caught it

fixed

[IceTDrinker]

perfect !

@IceTDrinker reviewed 1 of 1 files at r10, all commit messages.
Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @mayeul-zama and @tmontaigu)