fix: :i8 vs :byte

[lorenzogentile404]

If we define (MSHP :i8) , we obtain new ColumnHeader("shfreftable.MSHP", 2, length) in Java (i.e., 2 bytes, while it should be 1). Instead, if we define (MSHP :byte) then we obtain new ColumnHeader("shfreftable.MSHP", 1, length), that is what I expected.

[OlivierBBB]

(slack comment) Could it be that i8 translates to 2 bytes because integers are naturally signed in Java ? So that in order to represent (nonnegative) 8bit integers you need 9 bits and so 2 bytes ?

[delehef]

Nearly, as can be seen here. This comes from unsigned bytes being very finicky to handle in Java, hence the choice to “waste” a byte, but use an integer type that will behave more intuitively.

[lorenzogentile404]

@OlivierBBB I have checked the specs and it says

MICRO_SHIFT_PARAM: counter-constant column with values in {0, 1, . . . , 7, 8}; abbreviated to μSHP;

thus :byte should be fine anyway. Also, @ivokub mentioned that with 2 bytes, Corset was complaining:

The validation in corset which fails is:
RawMagma::Integer(b) => {
if x.bit_size() > *b {
bail!(RuntimeError::InvalidValue("integer", x))
} else {
Ok(x)
}
Imo it should be, I think the issue is that 0 is represented more than 8 bits. The condition which fails is x.bit_size() > *b
And imo for me it seems it is caused that we use field element representation instead of integer representation, and for field element representation bit_size()==254 always

So, while reducing the size of MSHP may solve the issue, I am not sure if this is the right way to solve it and there is something structurally wrong. @ivokub what do you think?

[DavePearce]

Could it be that i8 translates to 2 bytes because integers are naturally signed in Java ? So that in order to represent (nonnegative) 8bit integers you need 9 bits and so 2 bytes ?

Whilst this is technically true, you can always represent them as bytes in the correct way. It does require a bit of Java trickery to do it correctly though.

[DavePearce]

This comes from unsigned bytes being very finicky to handle in Java

Right, yeah. I have experience with this though. So, I can fix it.

[DavePearce]

@lorenzogentile404 Are we getting concerned about the size of trace files?

[DavePearce]

@lorenzogentile404 @delehef Ok, I put together a patch on the branch 158-fix-i8-vs-byte which you can view here. Feedback appreciated because, to be honest, its a bit hard for me to test this. It compiles at least within the linea-arithmetization project.

In the end, I just followed the existing implementation for byte which uses UnsignedByte to manage the encoding issues. Therefore, no trickery required :)

Thoughts?

[letypequividelespoubelles]

commented, imho we should separate the case :i1 which is in both case 1 and case 1..8.
Well, I think we never use the :i1 typing but ...

[ivokub]

So, while reducing the size of MSHP may solve the issue, I am not sure if this is the right way to solve it and there is something structurally wrong. @ivokub what do you think?

I'm not sure, to be honest. When I was printing values for x.bit_size() and b in the validation logic:

RawMagma::Integer(b) => {
    if x.bit_size() > *b {
        bail!(RuntimeError::InvalidValue("integer", x))
    } else {
        Ok(x)
    }

then x.bit_size() was 254 and b was 8, but I do not know how the Java types get mapped to in traces.

[DavePearce]

commented, imho we should separate the case :i1 which is in both case 1 and case 1..8.
Well, I think we never use the :i1 typing but ...

Ok, that's a fair point. Technically it will always choose the first case in the order so there is no ambiguity. But still better to be explicit about it. I will correct that.

[DavePearce]

Ok, corrected on the branch 158-fix-i8-vs-byte -- here.

[DavePearce]

then x.bit_size() was 254 and b was 8, but I do not know how the Java types get mapped to in traces.

Ok, @ivokub I feel like there is some missing context here. What's actually going on here? Is that line of code triggering a panic? For which module?

I see that sequence is in src/compiler/types.rs.

[DavePearce]

@delehef Also looking back at the code for the besu exporter, I realised it looks odd:

            1 => format!("{}.put((byte) (b ? 1 : 0));", &register),
            2..=8 => format!("{}.put(b.toByte());", &register),
            9..=15 => format!("{}.putShort(b);", &register),
            16..=31 => format!("{}.putInt(b);", &register),
            32..=63 => format!("{}.putLong(b);", &register),

For example, 9..=15. I'm assuming this is related to the fact that short is signed. But, it seems like the API could work around this?

EDIT: am just trying to figure out how this is all working 🤔

Ok, so case in point. From wcp/Trace.java:

public Trace wordComparisonStamp(final long b) {
    ...
    wordComparisonStamp.putLong(b);
   ...
  }

This is called from WcpOperation.java:

void trace(Trace trace, int stamp) {
    ...
    for (int ct = 0; ct <= this.maxCt(); ct++) {
      trace
          .wordComparisonStamp(stamp)

Which in turn is called from Wcp.java:

  public void commit(List<MappedByteBuffer> buffers) {
    final Trace trace = new Trace(buffers);

    int stamp = 0;
    for (WcpOperation operation : this.operations) {
      stamp++;
      operation.trace(trace, stamp);
    }
  }

So, stamp is an int anyway? Anyway, not actually relevant for this issue I guess.

[ivokub]

So, for the context - I had received a trace and zkevm.bin and was trying to load the trace in Go for testing the prover. The code for importing traces is:

	trace, err := C.trace_compute_from_file(
		corset,
		C.CString("/home/ivo/temp/cur/1_1672648872179459994.lt"),
		C.uint(numberOfThreads),
		false,
	)

doing this, I received the error

while computing from file `/home/ivo/temp/cur/1_1672648872179459994.lt`

Caused by:
    0: reading data for shfreftable.MSHP (2304 elts. expected)
    1: reading 0th element
    2: expected a integer value, found 0

It looks like the validation was happening in the snippet in src/compiler/types.rs. When I'm trying to print:

            RawMagma::Integer(b) => {
                if x.bit_size() > *b {
                    println!("{} > {}: {}", x.bit_size(), b, x);
                    bail!(RuntimeError::InvalidValue("integer", x))
                } else {
                    Ok(x)
                }
            }

then I see:

254 > 8: 0

So the value is 0, it is expected to be represented by 8 bits but is represented by 254 bits. It would make sense for me if the value x is not represented as big integer, but as a field element (in column.rs):

pub enum Value {
    BigInt(BigInt),
    #[serde(with = "FrDef")]
    Native(Fr),
    #[serde(skip)]
    ExoNative(Vec<Fr>),
}

    pub(crate) fn bit_size(&self) -> usize {
        match self {
            Value::BigInt(i) => i.bits() as usize,
            Value::Native(_) => crate::constants::FIELD_BITSIZE,
            Value::ExoNative(fs) => fs.len() * crate::constants::FIELD_BITSIZE,
        }
    }

@lorenzogentile404 has sent me new traces, I'll check with them. But if it only omits the module, then I think that the underlying issue (the column is defined as :i8, but we use field elements in the trace) is still unresolved.

(sorry if I have missed something which has already been fixed)

[ivokub]

And this still appears with the update trace but in a different location (now failing where we have a colum defined as :i3).

I'm uploading the zkevm.bin and the trace I have received, the corresponding method in Rust is trace_compute_from_file in lib.rs.

https://drive.google.com/file/d/1kTtALDaoRYqlvQ07P26kld_9DWxPlDOA/view?usp=sharing, https://drive.google.com/file/d/1sVIYWxtcf-iomzlBhj7izT-LtraPdPNF/view?usp=sharing

[delehef]

So, stamp is an int anyway?

It should be automatically casted to a long when invoking the method, as it takes a long.

[delehef]

@ivokub are you 100% that versions of the corset you use to check, the corset that was used to generate the Java API, the constraints you use, and the constraints that were used to generate the java traces are all the same?

[lorenzogentile404]

@delehef zkevm.bin was generated with corset 9.7.10 067b412 and by running corset check it works on my machine. The problem arises when @ivokub tries to read the .lt file programmatically. By Java API you mean the Trace.java file? Also, I do not get what you mean by

the constraints you use, and the constraints that were used to generate the java traces

[ivokub]

I'm using the same corset version 067b412 to read the trace. zkevm.bin and traces are provided by @lorenzogentile404 and with the versions above

[DavePearce]

It should be automatically casted to a long when invoking the method, as it takes a long

Yeah, I understand that. I'm just not sure why it is being upgraded?

From what I can understand of this issue, the problem is that e.g. 2 bytes are being packed into an lt trace for an i8 when corset is expecting at most 8bits ... so its throwing a wobbly. Is that about right?

But then i'm even more confused. Because, basically, anytime we're using e.g. and i32 or an i64 in the constraints the same thing is gonna happen, no? It'll pack 8bytes for an i32 ... which corset will not like. So ... whats changed thats exposed this issue now?

Anyways, I'm aways to Zzzz now. Can revisit this on Monday.

[lorenzogentile404]

@DavePearce @ivokub I suggest to have a call about this on Monday, so as we can ensure we are all on the same page regarding the issues we need to address and what has been done up to now.

[DavePearce]

by running corset check it works on my machine

@lorenzogentile404 Are you running corset check with the switch -N here? That might be the difference.

[lorenzogentile404]

No, I did not. What is it for? Now I get the same error @ivokub got at least.

corset check -N --trace 1_15024091914360580354.lt zkevm.bin
Error: while expanding `1_15024091914360580354.lt`

Caused by:
    0: reading data for ecdata.CT (10 elts. expected)
    1: reading 0th element
    2: expected a integer value, found 0

[DavePearce]

So the value is 0, it is expected to be represented by 8 bits but is represented by 254 bits

@ivokub Thanks, the context is helping. Presumably, one way this could arise would be if the trace was generated for a zkevm.bin where the column in question was not annotated with e.g. :i8. Then, if you try to load the trace in using a zkevm.bin file where that column is now annotated :i8 you would see this behaviour. But, there are probably other possible explanations as well. I will have to look into it on Monday.

@lorenzogentile404 Call on Monday morning European time can work for me --- just put something in the calendar. That'll be Monday evening for me, so I will have had a chance to get up to speed with this :)

[DavePearce]

No, I did not. What is it for? Now I get the same error @ivokub got at least.

Yay, progress :)

The -N switch tells Corset to check using finite fields rather than big integers. Still, its confusing me what's actually going on here. It might just be a bug.

[delehef]

I'm just not sure why it is being upgraded?

Depends on how the column is declared in the constraints.

[delehef]

the constraints you use, and the constraints that were used to generate the java traces

@lorenzogentile404 I mean the version of the constraints used to generate the Trace.java file, and the one used to generate the zkevm.bin that Ivo uses.

[DavePearce]

Depends on how the column is declared in the constraints.

I think in this case STAMP is declared i32, which is consistent with Corset translating it as a lo ng.

[delehef]

Yep, that's why.

[DavePearce]

Yep, that's why.

Right, but doesn't it seem odd? Int -> int -> long -> 8bytes -> field representing int (i32).

Anyways, no dramas. I need to study the trace filling in more detail.

[DavePearce]

Ok, some concrete data / from the traces / zkevm.bin provided by @lorenzogentile404:

• corset check -N gives this failure:

Error: while expanding `3_4376965835379734770.lt`

Caused by:
    0: reading data for ecdata.CT (10 elts. expected)
    1: reading 0th element
    2: expected a integer value, found 0

• In the tracefile, I can see that ecdata.CT has 2 bytes per element (which most likely corresponds to i8).
• In commit df0e5e5 of the constraints, I find this:

(defcolumns
  ...
  (CT :i3@prove)

Overall, that looks consistent with two explanations:

1. Tracefile was generated for old zkevm.bin file.
2. There is some bug related to handling of i3 in corset.

I will investigate (2) now. Actually, I think its the most likely as well, since older versions of ecdata didn't even have a CT column.

UPDATE: Can also confirm that at the offending line:

          RawMagma::Integer(b) => {
                if x.bit_size() > *b {
                    println!("BITWIDTH: {}, B: {b}",x.bit_size());
                    bail!(RuntimeError::InvalidValue("integer", x))
                } else {
                    Ok(x)
                }
            }

We get BITWIDTH: 254, B: 3. That does seem confusing.

UPDATE: Can also eliminate the zkevm.bin as being the problem. Digging into it, I extracted this:

(register:Some(166),padding_value:None,used:true,must_prove:true,kind:Commitment,t:(m:Integer(3),c:None),intrinsic_size_factor:None,base:Hex,handle:(module:"ecdata",name:"CT",perspective:None),computed:false)

Which is consistent with i3 as the type for CT.

[DavePearce]

Ok, I have a minimal test case now for reproduction:

(module test)
(defcolumns (X :i3))
(defconstraint test () (* (eq! X 1) (eq! X 2) (eq! X 3) (eq! X 4)))

Using a generated trace file containing column test.X with 2 bytes per element and a single value of 123 ... causes the error above (see attached lt file with the given txt extension). The upshot is that I didn't manage to get any trace accepted by corset check involving an iX type, including i4, i8 and i16. However, I do get a trace involving a :byte type to be accepted.

test.txt

[DavePearce]

Also, worth noting, when corset is being used to check the constraints in the arithmetization repository, it is being run without the -N option. Which helps answer the question I raised before:

But then i'm even more confused. Because, basically, anytime we're using e.g. and i32 or an i64 in the constraints the same thing is gonna happen, no? It'll pack 8bytes for an i32 ... which corset will not like. So ... whats changed thats exposed this issue now?

[DavePearce]

So, the very rough sequence is:

1. Value read initially as BigInt
2. Value then coerced into a Value which (when -N is given) wraps it into a native field value:

impl TryFrom<BigInt> for Value {
    type Error = errors::RuntimeError;

    fn try_from(int: BigInt) -> Result<Self, Self::Error> {
        if int.bits() as usize > constants::FIELD_BITSIZE {
            return Err(errors::RuntimeError::InvalidValue(
                "field element",
                Value::BigInt(int),
            ));
        }
        let mut v = Value::BigInt(int);
        if *crate::IS_NATIVE.read().unwrap() {
            v.to_native();
        }
        Result::Ok(v)
    }
}

3. Then, the Value.bit_size() returned for a Value::Native instance is always 254.

So, the validation logic seems to be broken when used in conjunction with the -N switch.

[DavePearce]

Ok, I've rolled back the optimisation around i8 using UnsignedByte instead of two bytes. This is a separate optimisation, not relevant to the actual problem. I'll raise an issue for that (though its not a priority unless we need to optimise the lt file sizes).

For this issue, I've put together a fix (see above) and raised a PR, inviting some reviewers. @delehef I couldn't seem to add you as a reviewer, but any comments from you would be appreciated.