Skip to content

Encoded program cannot be decoded #286

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
uncomputable opened this issue Apr 5, 2025 · 15 comments · Fixed by #289
Closed

Encoded program cannot be decoded #286

uncomputable opened this issue Apr 5, 2025 · 15 comments · Fixed by #289

Comments

@uncomputable
Copy link
Collaborator

uncomputable commented Apr 5, 2025

Calling encode_to_vec and then RedeemNode::decode on the following program leads to a type unification error.

See BlockstreamResearch/simfony#118

Decode(Type(Bind { existing_bound: { tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × ({ tmr: fd75bcd8cb55a5e424e09288ac8eb42942534ec1099b72bece0ea2c5479bf3e7, bit_width: 64, bound: 2^64 } × (... × ...))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), new_bound: { tmr: 50b38cd76475ff8929288bfcd0d9df0e4a241c0a5708572ad264192a4fe67bee, bit_width: 0, bound: 1 }, hint: "comp combinator: left target = right source" }))

The Simplicity program is obtained by compiling the following Simfony 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));
}

Calling encode_to_vec yields the following hex string (unpruned, without debug symbols):

e2a4d900000000022c8000000041805481420c31206b1566dc41180459000000010342c80000000c1a82a40a05bf203601acfc10c13481c040e0027063f0c040b480a0dc170601903888

The fact that the encoding is broken makes it hard to describe the problematic Simplicity program in this issue. For now, the Simfony compiler must be used to obtain it.

For now, the code to reproduce the error lives on this Simfony branch. Run cargo test --all-features.

@roconnor-blockstream
Copy link

roconnor-blockstream commented Apr 8, 2025

The deserialized code for this program is as follows. I've adjusted the references to refer to absolute line numbers instead of relative line numbers to make reading the code "easier".

0: Unit ()
1: Jet (SomeArrow (ConstWordJet 0: 2^32))
2: Comp () () () 0 1
3: Jet (SomeArrow (ConstWordJet 1: 2^32))
4: Comp () () () 0 3
5: Pair () () () 2 4
6: Iden ()
7: Pair () () () 5 6
8: Iden ()
9: Take () () () 8
10: Take () () () 9
11: Unit ()
12: Comp () () () 11 1
13: Pair () () () 10 12
14: Jet (SomeArrow (CoreJet (WordJet Eq32)))
15: Comp () () () 13 14
16: Jet (SomeArrow (CoreJet (WordJet Verify)))
17: Comp () () () 15 16
18: Jet (SomeArrow (ConstWordJet 2: 2^32))
19: Comp () () () 11 18
20: Jet (SomeArrow (ConstWordJet 3: 2^32))
21: Comp () () () 11 20
22: Pair () () () 19 21
23: Iden ()
24: Pair () () () 22 23
25: Pair () () () 10 19
26: Comp () () () 25 14
27: Comp () () () 26 16
28: Drop () () () 8
29: Take () () () 28
30: Pair () () () 29 21
31: Comp () () () 30 14
32: Comp () () () 31 16
33: Pair () () () 32 11
34: Drop () () () 6
35: Comp () () () 33 34
36: Pair () () () 27 35
37: Comp () () () 36 34
38: Comp () () () 24 37
39: Pair () () () 17 38
40: Comp () () () 39 34
41: Comp () () () 7 40

My analysis using the Haskell library is that type inference fails at 38: Comp () () () 24 37 with an occurs check failure. It fails "at" this line in the sense that the prefix does pass type inference. But, as typical for type inference errors, the ultimate source of the error may be earlier.

The occurs check fails due to trying to unify α with ((β × β) × α), where α and β are type variables used during inference.

I'll continue to look into this.

@roconnor-blockstream
Copy link

Based on a combination of inspecting the above "assembly code" and hand computing the Simfony to Simplicity compilation process, I believe the following is the the Simplicity program that should be generated (modulo any errors I have made)

let { e1 = ((unit >>> constWord 0) &&& (unit >>> constWord 1)); 
      e2 = ((ooh &&& (unit >>> constWord 0)) >>> eq32) >>> verify;
      e3 = ((unit >>> constWord 2) &&& (unit >>> constWord 3)); 
      e4 = ((ooh &&& (unit >>> constWord 2)) >>> eq32) >>> verify; 
      e5 = ((ooh &&& (unit >>> constWord 3)) >>> eq32) >>> verify } 
in (e1 &&& iden) >>> (e2 &&& ((e3 &&& iden) >>> (e4 &&& ((e5 &&& unit) >>> ih) >>> ih)) >>> ih)

The generated untyped program seems correct, which suggests there is an error in the rust-simplicity's optimal expression sharing implementation.

I'll continue to look into this.

@roconnor-blockstream
Copy link

It looks to me like that for some reason rust-simplicity is improperly implementing sharing when serializing this expression.

13: Pair 10 12

This line is (ooh &&& (unit >>> constWord 0)) and implements the (a,0) part of the assert!(jet::eq_32(a, 0)); line.
It should operate in the context of (W32 × W32) × 𝟙, which binds the simfony variables a and b at that point in the program. In other words, this Simplicity should have input type (W32 × W32) × 𝟙

In particular, line 10

10: Take 9

implements ooh : (W32 × W32) × 𝟙 ⊢ W32 , which implements the a part of (a,0); it reads the value that a is bound to from the context (W32 × W32) × 𝟙.

Later on, on line 25

25: Pair 10 19

this line is (ooh &&& (unit >>> constWord 2)) and implements the (c,2) part of the assert!(jet::eq_32(c, 2)); line. However, at this point in the Simfony program, the context is different as now c and d are also in scope. The context at this point of the Simfony program is (W32 × W32) × ((W32 × W32) × 𝟙), which contains the binding of ((c,d),((a,b),())) in that order. This Simplicity should have input type (W32 × W32) × ((W32 × W32) × 𝟙)

This time around ooh : (W32 × W32) × ((W32 × W32) × 𝟙) ⊢ W32 implements the c part of (c,2). Notice that although this bit of code, ooh, is the same for implementing c on this line, and for implementing a on the prior line, they operate in different environments and thus have different types. Because they have different input types, they ought to have different IHRs, and thus should not be shared.

How they ended up being shared, I don't know. Either the type inference is somehow wrong, and they ended up incorrectly with the same typed, and therefore shared, or the sharing implementation is somehow wrong.

Not that the unit subexpression from (ooh &&& (unit >>> constWord 0)) and (ooh &&& (unit >>> constWord 2)) have the same potential issue. In the first case we have an instance of unit : (W32 × W32) × 𝟙 ⊢𝟙, and in the second case we have an instance of unit : (W32 × W32) × ((W32 × W32) × 𝟙) ⊢𝟙, and thus the two units shouldn't be shared. But this time the implementation is correct: If you follow the children of 13: Pair 10 12, it leads to 0: Unit, while if you follow the children of 25: Pair 10 19 it leads to 11: Unit.

Why the unit case is correctly not shared, while the ooh is incorrectly shared, I have no idea.

@uncomputable
Copy link
Collaborator Author

Thanks for this detailed report. Maybe rust-simplicity is using the wrong Merkle root for sharing, or something.

@roconnor-blockstream
Copy link

roconnor-blockstream commented Apr 10, 2025

I've got the following program to fail

fn main() {
    let _ : () = ();
    {let _ : () = (); ()};

    let c : () = ();
    c;
    c;
}

With hex_encoding e06940a1281424102c703681333ea040b00141985a40640e00

@roconnor-blockstream
Copy link

I think there are really two bugs here. The first bug is that decoding this encoded program should throw a occurs-check failure instead of panicking with what appears to be a stack overflow. The second bug is that we shouldn't be generating ill-typed programs.

@roconnor-blockstream
Copy link

roconnor-blockstream commented Apr 11, 2025

Decoding of smaller program (with relative references changed to absolute references):

0: Unit ()
1: Iden ()
2: Pair () () () 0 1
3: Unit ()
4: Iden ()
5: Pair () () () 3 4
6: Unit ()
7: Comp () () () 5 6
8: Pair () () () 3 4
9: Take () () () 1
10: Pair () () () 9 3
11: Drop () () () 1
12: Comp () () () 10 11
13: Pair () () () 9 12
14: Comp () () () 13 11
15: Comp () () () 8 14
16: Pair () () () 7 15
17: Comp () () () 16 11
18: Comp () () () 2 17

@apoelstra
Copy link
Collaborator

When I construct the above using rust-simplicity directly I get a type mismatch error (left target = right source) on the final comp.

I manually double-checked and checked with ChatGPT that my mapping from your Haskell to Rust code was faithful.

@apoelstra
Copy link
Collaborator

Error comp combinator: left target = right source
Existing bound: 1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (1 × (... × ...)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     New bound: 1

Lemme dig into how simfony is managing to construct this..

@roconnor-blockstream
Copy link

Try to construct a fully-unshared program in rust simplicity. That way we can test the sharing mechanism used during serialization.

Assuming I did the hand construction correctly the unshared program (in Haskell syntax) is

(unit &&& iden) >>> ((((unit &&& iden)>>>unit)&&&((unit &&& iden) >>> (oh&&&(oh&&&unit>>>ih)>>>ih)))>>>ih)

@apoelstra
Copy link
Collaborator

I wasn't able to make any progress doing that -- I can't cajole rust-simplicity misbehave.

I am now investigating named::to_commit_node. This function dates to the initial commit of this library, when it was a "forgetful functor" mapping a NamedCommitNode to CommitNode by dropping all the name data. However, in b2e51f2df44d844cefc9604a7a531e3ef2ef1d95 (commit 8 of the 15-commit BlockstreamResearch/simfony#63) we replaced NamedCommitNode with NamedConstructNode while largely preserving this function.

It appears that the logic of to_commit_node is now equivalent to the logic of rust-simplicity's ConstructNode::finalize_types function. This is very different from "just forget all the names". But the comments surrounding this function, and the auxiliary structs used with in it, still say that this is purely a forgetful mapping. So at the very least this code needs to be renamed and recommented.

@apoelstra
Copy link
Collaborator

Ok, can reproduce in rust-simplicity with

diff --git a/src/node/construct.rs b/src/node/construct.rs
index ec7ef93..55ad8e6 100644
--- a/src/node/construct.rs
+++ b/src/node/construct.rs
@@ -517,4 +517,54 @@ mod tests {
                 .cmr()
         );
     }
+
+    #[test]
+    fn regression_286() {
+        use crate::bitcoin::hex::DisplayHex as _;
+        let ctx = types::Context::new();
+
+            let u0 = Arc::<ConstructNode<Core>>::unit(&ctx);
+        let i1 = Arc::<ConstructNode<Core>>::iden(&ctx);
+        let p2 = Arc::<ConstructNode<Core>>::pair(&u0, &i1).unwrap();
+        let u3 = Arc::<ConstructNode<Core>>::unit(&ctx);
+        let i4 = Arc::<ConstructNode<Core>>::iden(&ctx);
+        let p5 = Arc::<ConstructNode<Core>>::pair(&u3, &i4).unwrap();
+        let u6 = Arc::<ConstructNode<Core>>::unit(&ctx);
+        let c7 = Arc::<ConstructNode<Core>>::comp(&p5, &u6).unwrap();
+        let u8 = Arc::<ConstructNode<Core>>::unit(&ctx);
+        let i9 = Arc::<ConstructNode<Core>>::iden(&ctx);
+        let p10 = Arc::<ConstructNode<Core>>::pair(&u8, &i9).unwrap();
+        let i11 = Arc::<ConstructNode<Core>>::iden(&ctx);
+        let t12 = Arc::<ConstructNode<Core>>::take(&i11);
+        let i13 = Arc::<ConstructNode<Core>>::iden(&ctx);
+        let t14 = Arc::<ConstructNode<Core>>::take(&i13);
+        let u15 = Arc::<ConstructNode<Core>>::unit(&ctx);
+        let p16 = Arc::<ConstructNode<Core>>::pair(&t14, &u15).unwrap();
+        let i17 = Arc::<ConstructNode<Core>>::iden(&ctx);
+        let d18 = Arc::<ConstructNode<Core>>::drop_(&i17);
+        let c19 = Arc::<ConstructNode<Core>>::comp(&p16, &d18).unwrap();
+        let p20 = Arc::<ConstructNode<Core>>::pair(&t12, &c19).unwrap();
+        let i21 = Arc::<ConstructNode<Core>>::iden(&ctx);
+        let d22 = Arc::<ConstructNode<Core>>::drop_(&i21);
+        let c23 = Arc::<ConstructNode<Core>>::comp(&p20, &d22).unwrap();
+        let c24 = Arc::<ConstructNode<Core>>::comp(&p10, &c23).unwrap();
+        let p25 = Arc::<ConstructNode<Core>>::pair(&c7, &c24).unwrap();
+        let i26 = Arc::<ConstructNode<Core>>::iden(&ctx);
+        let d27 = Arc::<ConstructNode<Core>>::drop_(&i26);
+        let c28 = Arc::<ConstructNode<Core>>::comp(&p25, &d27).unwrap();
+        let c29 = Arc::<ConstructNode<Core>>::comp(&p2, &c28).unwrap();
+
+        let finalized: Arc<CommitNode<_>> = c29.finalize_types().unwrap();
+        let finalized: Arc<RedeemNode<_>> = finalized.finalize(&mut crate::node::SimpleFinalizer::new(core::iter::empty())).unwrap();
+        let (prog, wit) = finalized.encode_to_vec();
+
+        println!("encoded prog: {}", prog.as_hex());
+
+        let prog = BitIter::from(prog);
+        let wit = BitIter::from(wit);
+        let decode = RedeemNode::<Core>::decode(prog, wit).unwrap(); // will panic here
+
+        assert_eq!(finalized, decode);
+
+    }
 }

I obtained this program by looking at the program produced internally by simfony before the call to to_commit_node. I then call finalize_types on this which produces the bad program. The expected behavior, is that finalize_types should fail. But instead it "succeeds" and produces a program that can be encoded but fails the occurs check on decode.

@roconnor-blockstream
Copy link

roconnor-blockstream commented Apr 11, 2025

Correction: The expected behavior is that finalize_types succeeds and that it correctly serializes and deserializes.

The correct shared DAG should be

0: Unit One
1: Iden One
2: Pair One One One 2 1
3: Unit (Prod One One)
4: Iden (Prod One One)
5: Pair (Prod One One) One (Prod One One) 2 1
6: Unit (Prod One (Prod One One))
7: Comp (Prod One One) (Prod One (Prod One One)) One 2 1
8: Take One (Prod One One) One 7
9: Pair (Prod One (Prod One One)) One One 1 3
10: Drop One One One 9
11: Comp (Prod One (Prod One One)) (Prod One One) One 2 1
12: Pair (Prod One (Prod One One)) One One 4 1
13: Comp (Prod One (Prod One One)) (Prod One One) One 1 3
14: Comp (Prod One One) (Prod One (Prod One One)) One 9 1
15: Pair (Prod One One) One One 8 1
16: Comp (Prod One One) (Prod One One) One 1 6
17: Comp One (Prod One One) One 15 1

And should be encoded as "e04940a1281424106cc4a7d2081600283485a00640de"

@apoelstra
Copy link
Collaborator

Quick update before we sign off for the weekend -- we have a working fix, but it was produced by Claude 3.7-sonnet (a LLM) and we aren't yet confident in its correctness or why it works.

@apoelstra
Copy link
Collaborator

Have fix up. Turn out the AI thing was a red herring. I'm just iterating on getting CI to pass (need to fix stuff for non-default features sets).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants