TypeInferenceUnification error when unpacking two pairs

[m-kus]

I get TypeInferenceUnification error when trying to run the following program:

fn main() {
    let (a, b): (u32, u32) = (0, 1);
    assert!(jet::eq_32(a, 0));

    let (c, d): (u32, u32) = (2, 3);
    assert!(jet::eq_32(c, 2));
    assert!(jet::eq_32(d, 3));
}

This does not reproduce in BitMachine (I suppose because it does not run type checking?) but only when using https://github.com/BlockstreamResearch/rust-simplicity/blob/33b043f9a153f0d7be82dee8fbd61179ad63b888/simplicity-sys/src/tests/mod.rs#L113 (which calls the same code as Elements node under the hood).

When I'm trying to disassemble I get:

Error: failed to decode program: failed to apply bound1to existing bound2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (2^64 × (... × ...))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))): comp combinator: left target = right source

[uncomputable]

Interesting. I couldn't reproduce the error on the Simfony IDE, but that website is running an older version. I will try the latest version next.

[m-kus]

Ok thanks! I'm using this cli tool, in case it might be handy:

cargo install --git https://github.com/keep-starknet-strange/stark-symphony --rev d552969f2c64ce9fa80dc6a45bab17a4f6204bc9 simfony-cli

Then to build & run:

simfony run main.simf
simfony build main.simf --output-format simpl

[uncomputable]

I could reproduce the error using your stark-symphony crate.

This bug might be related to issues on Windows (BlockstreamResearch/rust-simplicity#274) or issues with values (BlockstreamResearch/rust-simplicity#275).

I am debugging and I will publish a new version of Simfony once I'm done. I will include a unit test with your program to prevent future regression.

[apoelstra]

I think this might fix it in rust-simplicity -- it fixes a regression I found in the padded bit iterator of Value. It's hard for me to go further because I need to backport BlockstreamResearch/rust-simplicity#271 so that I stop crashing the release version :)

diff --git a/src/value.rs b/src/value.rs
index 3aea277..0d58f81 100644
--- a/src/value.rs
+++ b/src/value.rs
@@ -358,10 +358,10 @@ impl Value {
         let total_width = cmp::max(inner.ty.bit_width(), right.bit_width());

         let (concat, concat_offset) = product(
-            Some((&inner.inner, inner.bit_offset)),
-            inner.ty.bit_width(),
             None,
             total_width - inner.ty.bit_width(),
+            Some((&inner.inner, inner.bit_offset)),
+            inner.ty.bit_width(),
         );
         let (new_inner, new_bit_offset) = right_shift_1(&concat, concat_offset, false);
         Self {

[uncomputable]

I feel we should merge the change into the upstream repo, so I can update simfony. See BlockstreamResearch/rust-simplicity#281

[apoelstra]

Yep, for sure! Was just posting the code here because I had to run, this was a somewhat-related open tab, and I didn't want to lose track of it. Thanks for opening the PR for me.

[apoelstra]

Reopening since it's apparently not fixed.

[uncomputable]

As far as Simfony is concerned, the bug is fixed. There is a passing unit test for this in the library.

@m-kus please reconfirm or correct me if I'm wrong.

[m-kus]

@uncomputable there seems to be two related problems disguising as one, let's close this issue and I'll create a new one if that works better

I created #117 to showcase the remaining problem (tbh I'm not fully sure it's on the Simfony side) and new issue #118

[apoelstra]

Thanks -- let's move to the other issue.