cairo-lang-lowering 2.18.0

//! > Test multiple snapshots of same variable creates equivalences

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: Array<felt252>) -> (@Array<felt252>, @Array<felt252>) {
    let snap1 = @x;
    let snap2 = @x;
    (snap1, snap2)
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::array::Array::<core::felt252>
blk0 (root):
Statements:
  (v1: core::array::Array::<core::felt252>, v2: @core::array::Array::<core::felt252>) <- snapshot(v0)
  (v3: core::array::Array::<core::felt252>, v4: @core::array::Array::<core::felt252>) <- snapshot(v1)
  (v5: (@core::array::Array::<core::felt252>, @core::array::Array::<core::felt252>)) <- struct_construct(v2, v4)
End:
  Return(v5)

//! > analysis_state
Block 0:
(@core::array::Array::<core::felt252>, @core::array::Array::<core::felt252>)(v2, v2) = v5, @v0 = v2, v0 = v1, v0 = v3, v2 = v4

//! > ==========================================================================

//! > Test simple function with no equality operations

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: felt252, y: felt252) -> felt252 {
    x + y
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252
blk0 (root):
Statements:
  (v2: core::felt252) <- core::felt252_add(v0, v1)
End:
  Return(v2)

//! > analysis_state
Block 0:
(empty)

//! > ==========================================================================

//! > Test chained snapshots track transitive equality

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: Array<felt252>) -> (@Array<felt252>, @Array<felt252>, @Array<felt252>) {
    let snap1 = @x;
    let snap2 = @x;
    let snap3 = @x;
    (snap1, snap2, snap3)
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::array::Array::<core::felt252>
blk0 (root):
Statements:
  (v1: core::array::Array::<core::felt252>, v2: @core::array::Array::<core::felt252>) <- snapshot(v0)
  (v3: core::array::Array::<core::felt252>, v4: @core::array::Array::<core::felt252>) <- snapshot(v1)
  (v5: core::array::Array::<core::felt252>, v6: @core::array::Array::<core::felt252>) <- snapshot(v3)
  (v7: (@core::array::Array::<core::felt252>, @core::array::Array::<core::felt252>, @core::array::Array::<core::felt252>)) <- struct_construct(v2, v4, v6)
End:
  Return(v7)

//! > analysis_state
Block 0:
(@core::array::Array::<core::felt252>, @core::array::Array::<core::felt252>, @core::array::Array::<core::felt252>)(v2, v2, v2) = v7, @v0 = v2, v0 = v1, v0 = v3, v0 = v5, v2 = v4, v2 = v6

//! > ==========================================================================

//! > Test box of same value creates box equivalence

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: felt252) -> (Box<felt252>, Box<felt252>) {
    let box1 = BoxTrait::new(x);
    let box2 = BoxTrait::new(x);
    (box1, box2)
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252
blk0 (root):
Statements:
  (v1: core::box::Box::<core::felt252>) <- into_box(v0)
  (v2: core::box::Box::<core::felt252>) <- into_box(v0)
  (v3: (core::box::Box::<core::felt252>, core::box::Box::<core::felt252>)) <- struct_construct(v1, v2)
End:
  Return(v3)

//! > analysis_state
Block 0:
(core::box::Box::<core::felt252>, core::box::Box::<core::felt252>)(v1, v1) = v3, Box(v0) = v1, v1 = v2

//! > ==========================================================================

//! > Test struct construct and destructure tracks equality

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(a: felt252, b: felt252) -> (MyStruct, felt252, felt252) {
    let s = MyStruct { x: a, y: b };
    let MyStruct { x, y } = s;
    (MyStruct { x, y }, x, y)
}

//! > function_name
foo

//! > module_code
#[derive(Drop, Copy)]
struct MyStruct {
    x: felt252,
    y: felt252,
}

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252
blk0 (root):
Statements:
  (v2: test::MyStruct) <- struct_construct(v0, v1)
  (v3: core::felt252, v4: core::felt252) <- struct_destructure(v2)
  (v5: test::MyStruct) <- struct_construct(v3, v4)
  (v6: (test::MyStruct, core::felt252, core::felt252)) <- struct_construct(v5, v3, v4)
End:
  Return(v6)

//! > analysis_state
Block 0:
(test::MyStruct, core::felt252, core::felt252)(v2, v0, v1) = v6, test::MyStruct(v0, v1) = v2, v0 = v3, v1 = v4, v2 = v5

//! > ==========================================================================

//! > Test enum construct tracks variant

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: felt252) -> MyEnum {
    MyEnum::A(x)
}

//! > function_name
foo

//! > module_code
#[derive(Drop)]
enum MyEnum {
    A: felt252,
    B: felt252,
}

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252
blk0 (root):
Statements:
  (v1: test::MyEnum) <- MyEnum::A(v0)
End:
  Return(v1)

//! > analysis_state
Block 0:
A(v0) = v1

//! > ==========================================================================

//! > Test match with diamond control flow loses equality info

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: felt252) -> felt252 {
    let snap1 = @x;
    let result = match x {
        0 => 1,
        _ => 2,
    };
    result
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics
warning[E0001]: Unused variable. Consider ignoring by prefixing with `_`.
 --> lib.cairo:2:9
    let snap1 = @x;
        ^^^^^

//! > lowering
Parameters: v0: core::felt252
blk0 (root):
Statements:
  (v1: core::felt252, v2: @core::felt252) <- snapshot(v0)
End:
  Match(match core::felt252_is_zero(v1) {
    IsZeroResult::Zero => blk1,
    IsZeroResult::NonZero(v3) => blk2,
  })

blk1:
Statements:
  (v4: core::felt252) <- 1
End:
  Return(v4)

blk2:
Statements:
  (v5: core::felt252) <- 2
End:
  Return(v5)

//! > analysis_state
Block 0:
@v0 = v2, v0 = v1

Block 1:
@v0 = v2, v0 = v1

Block 2:
@v0 = v2, v0 = v1

//! > ==========================================================================

//! > Test match on Option with diamond merges conservatively

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(opt: Option<felt252>) -> felt252 {
    match opt {
        Option::Some(val) => val,
        Option::None => 0,
    }
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::option::Option::<core::felt252>
blk0 (root):
Statements:
End:
  Match(match_enum(v0) {
    Option::Some(v1) => blk1,
    Option::None(v2) => blk2,
  })

blk1:
Statements:
End:
  Return(v1)

blk2:
Statements:
  (v3: core::felt252) <- 0
End:
  Return(v3)

//! > analysis_state
Block 0:
(empty)

Block 1:
Some(v1) = v0

Block 2:
None(v2) = v0

//! > ==========================================================================

//! > Test equality preserved within single match arm

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(arr: Array<felt252>) -> @Array<felt252> {
    match arr.len() {
        0 => {
            let snap = @arr;
            snap
        },
        _ => {
            let snap = @arr;
            snap
        },
    }
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::array::Array::<core::felt252>
blk0 (root):
Statements:
  (v1: core::array::Array::<core::felt252>, v2: @core::array::Array::<core::felt252>) <- snapshot(v0)
  (v3: core::integer::u32) <- core::array::array_len::<core::felt252>(v2)
  (v4: core::felt252) <- core::internal::bounded_int::upcast::<core::integer::u32, core::felt252>(v3)
End:
  Match(match core::felt252_is_zero(v4) {
    IsZeroResult::Zero => blk1,
    IsZeroResult::NonZero(v5) => blk2,
  })

blk1:
Statements:
  (v6: core::array::Array::<core::felt252>, v7: @core::array::Array::<core::felt252>) <- snapshot(v1)
End:
  Return(v7)

blk2:
Statements:
  (v8: core::array::Array::<core::felt252>, v9: @core::array::Array::<core::felt252>) <- snapshot(v1)
End:
  Return(v9)

//! > analysis_state
Block 0:
@v0 = v2, v0 = v1

Block 1:
@v0 = v2, v0 = v1, v0 = v6, v2 = v7

Block 2:
@v0 = v2, v0 = v1, v0 = v8, v2 = v9

//! > ==========================================================================

//! > Test nested box operations

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: felt252) -> (Box<Box<felt252>>, felt252) {
    let box1 = BoxTrait::new(x);
    let box2 = BoxTrait::new(box1);
    let unbox1 = box2.unbox();
    let unbox2 = unbox1.unbox();
    // Return both to prevent optimization from eliminating the boxes
    (box2, unbox2)
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252
blk0 (root):
Statements:
  (v1: core::box::Box::<core::felt252>) <- into_box(v0)
  (v2: core::box::Box::<core::box::Box::<core::felt252>>) <- into_box(v1)
  (v3: core::box::Box::<core::felt252>) <- unbox(v2)
  (v4: core::felt252) <- unbox(v3)
  (v5: (core::box::Box::<core::box::Box::<core::felt252>>, core::felt252)) <- struct_construct(v2, v4)
End:
  Return(v5)

//! > analysis_state
Block 0:
(core::box::Box::<core::box::Box::<core::felt252>>, core::felt252)(v2, v0) = v5, Box(v0) = v1, Box(v1) = v2, v0 = v4, v1 = v3

//! > ==========================================================================

//! > Test snapshot of boxed value

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: Array<felt252>) -> @Box<@Array<felt252>> {
    let snap = @x;
    let boxed = BoxTrait::new(snap);
    let box_snap = @boxed;
    box_snap
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::array::Array::<core::felt252>
blk0 (root):
Statements:
  (v1: core::array::Array::<core::felt252>, v2: @core::array::Array::<core::felt252>) <- snapshot(v0)
  (v3: core::box::Box::<@core::array::Array::<core::felt252>>) <- into_box(v2)
  (v4: core::box::Box::<@core::array::Array::<core::felt252>>, v5: @core::box::Box::<@core::array::Array::<core::felt252>>) <- snapshot(v3)
End:
  Return(v5)

//! > analysis_state
Block 0:
@v0 = v2, @v3 = v5, Box(v2) = v3, v0 = v1, v3 = v4

//! > ==========================================================================

//! > Test reboxing through function call

//! > TODO(eytan-starkware): Inter-procedural analysis to track equality through function calls

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(boxed: Box<felt252>) -> Box<felt252> {
    let unboxed = boxed.unbox();
    let modified = identity(unboxed);
    let reboxed = BoxTrait::new(modified);
    reboxed
}

//! > function_name
foo

//! > module_code
#[inline(never)]
fn identity(x: felt252) -> felt252 {
    x
}

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::box::Box::<core::felt252>
blk0 (root):
Statements:
  (v1: core::felt252) <- unbox(v0)
  (v2: core::felt252) <- test::identity(v1)
  (v3: core::box::Box::<core::felt252>) <- into_box(v2)
End:
  Return(v3)

//! > analysis_state
Block 0:
Box(v1) = v0, Box(v2) = v3

//! > ==========================================================================

//! > Test enum construct with same variant across branches preserves info after merge

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(cond: bool, x: felt252) -> felt252 {
    // Construct same enum variant in both branches
    let e = if cond {
        MyEnum::A(x)
    } else {
        MyEnum::A(x)
    };

    // Force the value to be used after merge
    use_enum(e);
    x
}

//! > function_name
foo

//! > module_code
#[derive(Drop)]
enum MyEnum {
    A: felt252,
    B: felt252,
}

#[inline(never)]
fn use_enum(e: MyEnum) {}

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::bool, v1: core::felt252
blk0 (root):
Statements:
End:
  Match(match_enum(v0) {
    bool::False(v2) => blk1,
    bool::True(v3) => blk2,
  })

blk1:
Statements:
  (v4: test::MyEnum) <- MyEnum::A(v1)
End:
  Goto(blk3, {v4 -> v5})

blk2:
Statements:
  (v6: test::MyEnum) <- MyEnum::A(v1)
End:
  Goto(blk3, {v6 -> v5})

blk3:
Statements:
  () <- test::use_enum(v5)
End:
  Return(v1)

//! > analysis_state
Block 0:
(empty)

Block 1:
A(v1) = v4, False(v2) = v0

Block 2:
A(v1) = v6, True(v3) = v0

Block 3:
A(v1) = v5

//! > ==========================================================================

//! > Test enum construct with different variants across branches loses enum info after merge

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(cond: bool, x: felt252, y: felt252) -> felt252 {
    // Construct different enum variants in branches
    let e = if cond {
        MyEnum::A(x)
    } else {
        MyEnum::B(y)
    };

    // Force the value to be used after merge
    use_enum(e);
    x
}

//! > function_name
foo

//! > module_code
#[derive(Drop)]
enum MyEnum {
    A: felt252,
    B: felt252,
}

#[inline(never)]
fn use_enum(e: MyEnum) {}

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::bool, v1: core::felt252, v2: core::felt252
blk0 (root):
Statements:
End:
  Match(match_enum(v0) {
    bool::False(v3) => blk1,
    bool::True(v4) => blk2,
  })

blk1:
Statements:
  (v5: test::MyEnum) <- MyEnum::B(v2)
End:
  Goto(blk3, {v5 -> v6})

blk2:
Statements:
  (v7: test::MyEnum) <- MyEnum::A(v1)
End:
  Goto(blk3, {v7 -> v6})

blk3:
Statements:
  () <- test::use_enum(v6)
End:
  Return(v1)

//! > analysis_state
Block 0:
(empty)

Block 1:
B(v2) = v5, False(v3) = v0

Block 2:
A(v1) = v7, True(v4) = v0

Block 3:
(empty)

//! > ==========================================================================

//! > Test reboxing through desnap - equality preserved

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(boxed: Box<felt252>) -> (@Box<felt252>, Box<felt252>) {
    let snap = @boxed;
    let desnapped = *snap;
    let unboxed = desnapped.unbox();
    let reboxed = BoxTrait::new(unboxed);
    (snap, reboxed)
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::box::Box::<core::felt252>
blk0 (root):
Statements:
  (v1: core::box::Box::<core::felt252>, v2: @core::box::Box::<core::felt252>) <- snapshot(v0)
  (v3: core::box::Box::<core::felt252>) <- desnap(v2)
  (v4: core::felt252) <- unbox(v3)
  (v5: core::box::Box::<core::felt252>) <- into_box(v4)
  (v6: (@core::box::Box::<core::felt252>, core::box::Box::<core::felt252>)) <- struct_construct(v2, v5)
End:
  Return(v6)

//! > analysis_state
Block 0:
(@core::box::Box::<core::felt252>, core::box::Box::<core::felt252>)(v2, v0) = v6, @v0 = v2, Box(v4) = v0, v0 = v1, v0 = v3, v0 = v5

//! > ==========================================================================

//! > Test reboxing works through snapshot - equality tracked correctly

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(boxed: Box<felt252>) -> Box<felt252> {
    let unboxed = boxed.unbox();
    let snap = @unboxed;
    use_snap(snap);
    let reboxed = BoxTrait::new(unboxed);
    reboxed
}

//! > function_name
foo

//! > module_code
#[inline(never)]
fn use_snap(x: @felt252) {}

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::box::Box::<core::felt252>
blk0 (root):
Statements:
  (v1: core::felt252) <- unbox(v0)
  (v2: core::felt252, v3: @core::felt252) <- snapshot(v1)
  () <- test::use_snap(v3)
  (v4: core::box::Box::<core::felt252>) <- into_box(v2)
End:
  Return(v4)

//! > analysis_state
Block 0:
@v1 = v3, Box(v1) = v0, v0 = v4, v1 = v2

//! > ==========================================================================

//! > Test reboxing with different type - no equality

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(boxed: Box<u32>) -> Box<felt252> {
    let unboxed: u32 = boxed.unbox();
    let converted: felt252 = unboxed.into();
    let reboxed = BoxTrait::new(converted);
    reboxed
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::box::Box::<core::integer::u32>
blk0 (root):
Statements:
  (v1: core::integer::u32) <- unbox(v0)
  (v2: core::felt252) <- core::integer::u32_to_felt252(v1)
  (v3: core::box::Box::<core::felt252>) <- into_box(v2)
End:
  Return(v3)

//! > analysis_state
Block 0:
Box(v1) = v0, Box(v2) = v3

//! > ==========================================================================

//! > Test empty struct construct

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo() -> (EmptyStruct, EmptyStruct) {
    let s1 = EmptyStruct {};
    let s2 = EmptyStruct {};
    (s1, s2)
}

//! > function_name
foo

//! > module_code
#[derive(Drop, Copy)]
struct EmptyStruct {}

//! > semantic_diagnostics

//! > lowering
Parameters:
blk0 (root):
Statements:
  (v0: test::EmptyStruct) <- struct_construct()
  (v1: test::EmptyStruct) <- struct_construct()
  (v2: (test::EmptyStruct, test::EmptyStruct)) <- struct_construct(v0, v1)
End:
  Return(v2)

//! > analysis_state
Block 0:
(test::EmptyStruct, test::EmptyStruct)(v0, v0) = v2, test::EmptyStruct() = v0, v0 = v1

//! > ==========================================================================

//! > Test nested struct construct

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(a: felt252) -> Outer {
    let inner = Inner { x: a };
    Outer { inner }
}

//! > function_name
foo

//! > module_code
#[derive(Drop, Copy)]
struct Inner {
    x: felt252,
}

#[derive(Drop, Copy)]
struct Outer {
    inner: Inner,
}

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252
blk0 (root):
Statements:
  (v1: test::Inner) <- struct_construct(v0)
  (v2: test::Outer) <- struct_construct(v1)
End:
  Return(v2)

//! > analysis_state
Block 0:
test::Inner(v0) = v1, test::Outer(v1) = v2

//! > ==========================================================================

//! > Test struct hashcons merges across branches when inputs are equivalent

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(arr: Array<felt252>, cond: bool) -> @MyStruct {
    let snap = @arr;
    let s = if cond {
        let s = MyStruct { a: snap };
        use_struct(@s);
        s
    } else {
        let s = MyStruct { a: snap };
        use_struct(@s);
        s
    };
    @s
}

//! > function_name
foo

//! > module_code
#[derive(Drop, Copy)]
struct MyStruct {
    a: @Array<felt252>,
}

#[inline(never)]
fn use_struct(s: @MyStruct) {}

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::array::Array::<core::felt252>, v1: core::bool
blk0 (root):
Statements:
  (v2: core::array::Array::<core::felt252>, v3: @core::array::Array::<core::felt252>) <- snapshot(v0)
End:
  Match(match_enum(v1) {
    bool::False(v4) => blk1,
    bool::True(v5) => blk2,
  })

blk1:
Statements:
  (v6: test::MyStruct) <- struct_construct(v3)
  (v7: test::MyStruct, v8: @test::MyStruct) <- snapshot(v6)
  () <- test::use_struct(v8)
End:
  Goto(blk3, {v7 -> v9})

blk2:
Statements:
  (v10: test::MyStruct) <- struct_construct(v3)
  (v11: test::MyStruct, v12: @test::MyStruct) <- snapshot(v10)
  () <- test::use_struct(v12)
End:
  Goto(blk3, {v11 -> v9})

blk3:
Statements:
  (v13: test::MyStruct, v14: @test::MyStruct) <- snapshot(v9)
End:
  Return(v14)

//! > analysis_state
Block 0:
@v0 = v3, v0 = v2

Block 1:
@v0 = v3, @v6 = v8, False(v4) = v1, test::MyStruct(v3) = v6, v0 = v2, v6 = v7

Block 2:
@v0 = v3, @v10 = v12, True(v5) = v1, test::MyStruct(v3) = v10, v0 = v2, v10 = v11

Block 3:
@v0 = v3, @v9 = v14, test::MyStruct(v3) = v9, v0 = v2, v9 = v13

//! > ==========================================================================

//! > Test array new and append tracked via struct hashcons

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(a: felt252, b: felt252) -> Array<felt252> {
    let mut arr = ArrayTrait::new();
    arr.append(a);
    arr.append(b);
    arr
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252
blk0 (root):
Statements:
  (v2: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
  (v3: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v2, v0)
  (v4: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v3, v1)
End:
  Return(v4)

//! > analysis_state
Block 0:
core::array::Array::<core::felt252>() = v2, core::array::Array::<core::felt252>(v0) = v3, core::array::Array::<core::felt252>(v0, v1) = v4

//! > ==========================================================================

//! > Test array pop_front recovers elements and merge works correctly

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(a: felt252, b: felt252) -> Array<felt252> {
    let mut arr = ArrayTrait::new();
    arr.append(a);
    arr.append(b);
    let result = match arr.pop_front() {
        Option::Some(val) => {
            let mut remaining = ArrayTrait::new();
            remaining.append(val);
            remaining
        },
        Option::None => { arr },
    };
    use_arr(@result);
    result
}

//! > function_name
foo

//! > module_code
extern fn use_arr(x: @Array<felt252>) nopanic;

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252
blk0 (root):
Statements:
  (v2: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
  (v3: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v2, v0)
  (v4: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v3, v1)
End:
  Match(match core::array::array_pop_front::<core::felt252>(v4) {
    Option::Some(v5, v6) => blk1,
    Option::None(v7) => blk2,
  })

blk1:
Statements:
  (v8: core::felt252) <- unbox(v6)
End:
  Goto(blk4, {v8 -> v9})

blk2:
Statements:
  (v10: ()) <- struct_construct()
  (v11: core::option::Option::<core::felt252>) <- Option::None(v10)
End:
  Match(match_enum(v11) {
    Option::Some(v12) => blk3,
    Option::None(v13) => blk5,
  })

blk3:
Statements:
End:
  Goto(blk4, {v12 -> v9})

blk4:
Statements:
  (v14: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
  (v15: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v14, v9)
End:
  Goto(blk6, {v15 -> v16})

blk5:
Statements:
End:
  Goto(blk6, {v7 -> v16})

blk6:
Statements:
  (v17: core::array::Array::<core::felt252>, v18: @core::array::Array::<core::felt252>) <- snapshot(v16)
  () <- test::use_arr(v18)
End:
  Return(v17)

//! > analysis_state
Block 0:
core::array::Array::<core::felt252>() = v2, core::array::Array::<core::felt252>(v0) = v3, core::array::Array::<core::felt252>(v0, v1) = v4

Block 1:
Box(v0) = v6, core::array::Array::<core::felt252>() = v2, core::array::Array::<core::felt252>(v0) = v3, core::array::Array::<core::felt252>(v0, v1) = v4, core::array::Array::<core::felt252>(v1) = v5, v0 = v8

Block 2:
()() = v10, None(v10) = v11, core::array::Array::<core::felt252>() = v2, core::array::Array::<core::felt252>(v0) = v3, core::array::Array::<core::felt252>(v0, v1) = v2, v2 = v4, v2 = v7

Block 3:
()() = v10, None(v10) = v11, Some(v12) = v11, core::array::Array::<core::felt252>() = v2, core::array::Array::<core::felt252>(v0) = v3, core::array::Array::<core::felt252>(v0, v1) = v2, v2 = v4, v2 = v7

Block 4:
core::array::Array::<core::felt252>() = v2, core::array::Array::<core::felt252>(v0) = v3, core::array::Array::<core::felt252>(v0, v1) = v4, core::array::Array::<core::felt252>(v9) = v15, v2 = v14

Block 5:
()() = v10, None(v10) = v11, core::array::Array::<core::felt252>() = v2, core::array::Array::<core::felt252>(v0) = v3, core::array::Array::<core::felt252>(v0, v1) = v2, v10 = v13, v2 = v4, v2 = v7

Block 6:
@v16 = v18, core::array::Array::<core::felt252>() = v2, core::array::Array::<core::felt252>(v0) = v3, core::array::Array::<core::felt252>(v0, v1) = v4, v16 = v17

//! > ==========================================================================

//! > Test chained snapshot pop_front recovers elements

//! > test_runner_name
test_equality_analysis

//! > We snapshot a and b before building the span so they have snapshot classes.

//! > This allows the analysis to track Box(@a)/Box(@b) relationships when popping.

//! > function_code
fn foo(a: felt252, b: felt252) {
    let mut arr = ArrayTrait::new();
    arr.append(a);
    arr.append(b);
    use_snap_felt(@a);
    use_snap_felt(@b);
    let mut span = arr.span();
    match span.pop_front() {
        Option::Some(first) => {
            use_snap_felt(first);
            match span.pop_front() {
                Option::Some(second) => { use_snap_felt(second); },
                Option::None => {},
            };
        },
        Option::None => {},
    };
}

//! > function_name
foo

//! > module_code
extern fn use_snap_felt(x: @felt252) nopanic;

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252
blk0 (root):
Statements:
  (v2: core::felt252, v3: @core::felt252) <- snapshot(v0)
  () <- test::use_snap_felt(v3)
  (v4: core::felt252, v5: @core::felt252) <- snapshot(v1)
  () <- test::use_snap_felt(v5)
  (v6: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
  (v7: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v6, v0)
  (v8: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v7, v1)
  (v9: core::array::Array::<core::felt252>, v10: @core::array::Array::<core::felt252>) <- snapshot(v8)
  (v11: core::array::Span::<core::felt252>) <- struct_construct(v10)
  (v12: @core::array::Array::<core::felt252>) <- struct_destructure(v11)
End:
  Match(match core::array::array_snapshot_pop_front::<core::felt252>(v12) {
    Option::Some(v13, v14) => blk1,
    Option::None(v15) => blk4,
  })

blk1:
Statements:
  (v16: @core::felt252) <- unbox(v14)
  (v17: core::array::Span::<core::felt252>) <- struct_construct(v13)
  () <- test::use_snap_felt(v16)
  (v18: @core::array::Array::<core::felt252>) <- struct_destructure(v17)
End:
  Match(match core::array::array_snapshot_pop_front::<core::felt252>(v18) {
    Option::Some(v19, v20) => blk2,
    Option::None(v21) => blk3,
  })

blk2:
Statements:
  (v22: @core::felt252) <- unbox(v20)
  () <- test::use_snap_felt(v22)
End:
  Return()

blk3:
Statements:
  (v23: ()) <- struct_construct()
End:
  Return()

blk4:
Statements:
  (v24: ()) <- struct_construct()
  (v25: core::array::Span::<core::felt252>) <- struct_construct(v15)
End:
  Return()

//! > analysis_state
Block 0:
@v0 = v3, @v1 = v5, @v8 = v10, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, v0 = v2, v1 = v4, v10 = v12, v8 = v9

Block 1:
@core::array::Array::<core::felt252>(v1) = v13, @v0 = v3, @v1 = v5, @v8 = v10, Box(v3) = v14, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, core::array::Span::<core::felt252>(v13) = v17, v0 = v2, v1 = v4, v10 = v12, v13 = v18, v3 = v16, v8 = v9

Block 2:
@core::array::Array::<core::felt252>() = v19, @core::array::Array::<core::felt252>(v1) = v13, @v0 = v3, @v1 = v5, @v8 = v10, Box(v3) = v14, Box(v5) = v20, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, core::array::Span::<core::felt252>(v13) = v17, v0 = v2, v1 = v4, v10 = v12, v13 = v18, v3 = v16, v5 = v22, v8 = v9

Block 3:
()() = v23, @core::array::Array::<core::felt252>() = v13, @core::array::Array::<core::felt252>(v1) = v13, @v0 = v3, @v1 = v5, @v8 = v10, Box(v3) = v14, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, core::array::Span::<core::felt252>(v13) = v17, v0 = v2, v1 = v4, v10 = v12, v13 = v18, v13 = v21, v3 = v16, v8 = v9

Block 4:
()() = v24, @core::array::Array::<core::felt252>() = v10, @v0 = v3, @v1 = v5, @v8 = v10, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, v0 = v2, v1 = v4, v10 = v12, v10 = v15, v11 = v25, v8 = v9

//! > ==========================================================================

//! > Test chained snapshot pop_back recovers elements

//! > test_runner_name
test_equality_analysis

//! > We snapshot a and b before building the span so they have snapshot classes.

//! > This allows the analysis to track Box(@a)/Box(@b) relationships when popping.

//! > function_code
fn foo(a: felt252, b: felt252) {
    let mut arr = ArrayTrait::new();
    arr.append(a);
    arr.append(b);
    use_snap_felt(@a);
    use_snap_felt(@b);
    let mut span = arr.span();
    match span.pop_back() {
        Option::Some(last) => {
            use_snap_felt(last);
            match span.pop_back() {
                Option::Some(second_last) => { use_snap_felt(second_last); },
                Option::None => {},
            };
        },
        Option::None => {},
    };
}

//! > function_name
foo

//! > module_code
extern fn use_snap_felt(x: @felt252) nopanic;

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252
blk0 (root):
Statements:
  (v2: core::felt252, v3: @core::felt252) <- snapshot(v0)
  () <- test::use_snap_felt(v3)
  (v4: core::felt252, v5: @core::felt252) <- snapshot(v1)
  () <- test::use_snap_felt(v5)
  (v6: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
  (v7: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v6, v0)
  (v8: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v7, v1)
  (v9: core::array::Array::<core::felt252>, v10: @core::array::Array::<core::felt252>) <- snapshot(v8)
  (v11: core::array::Span::<core::felt252>) <- struct_construct(v10)
  (v12: @core::array::Array::<core::felt252>) <- struct_destructure(v11)
End:
  Match(match core::array::array_snapshot_pop_back::<core::felt252>(v12) {
    Option::Some(v13, v14) => blk1,
    Option::None(v15) => blk4,
  })

blk1:
Statements:
  (v16: @core::felt252) <- unbox(v14)
  (v17: core::array::Span::<core::felt252>) <- struct_construct(v13)
  () <- test::use_snap_felt(v16)
  (v18: @core::array::Array::<core::felt252>) <- struct_destructure(v17)
End:
  Match(match core::array::array_snapshot_pop_back::<core::felt252>(v18) {
    Option::Some(v19, v20) => blk2,
    Option::None(v21) => blk3,
  })

blk2:
Statements:
  (v22: @core::felt252) <- unbox(v20)
  () <- test::use_snap_felt(v22)
End:
  Return()

blk3:
Statements:
  (v23: ()) <- struct_construct()
End:
  Return()

blk4:
Statements:
  (v24: ()) <- struct_construct()
  (v25: core::array::Span::<core::felt252>) <- struct_construct(v15)
End:
  Return()

//! > analysis_state
Block 0:
@v0 = v3, @v1 = v5, @v8 = v10, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, v0 = v2, v1 = v4, v10 = v12, v8 = v9

Block 1:
@core::array::Array::<core::felt252>(v0) = v13, @v0 = v3, @v1 = v5, @v8 = v10, Box(v5) = v14, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, core::array::Span::<core::felt252>(v13) = v17, v0 = v2, v1 = v4, v10 = v12, v13 = v18, v5 = v16, v8 = v9

Block 2:
@core::array::Array::<core::felt252>() = v19, @core::array::Array::<core::felt252>(v0) = v13, @v0 = v3, @v1 = v5, @v8 = v10, Box(v3) = v20, Box(v5) = v14, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, core::array::Span::<core::felt252>(v13) = v17, v0 = v2, v1 = v4, v10 = v12, v13 = v18, v3 = v22, v5 = v16, v8 = v9

Block 3:
()() = v23, @core::array::Array::<core::felt252>() = v13, @core::array::Array::<core::felt252>(v0) = v13, @v0 = v3, @v1 = v5, @v8 = v10, Box(v5) = v14, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, core::array::Span::<core::felt252>(v13) = v17, v0 = v2, v1 = v4, v10 = v12, v13 = v18, v13 = v21, v5 = v16, v8 = v9

Block 4:
()() = v24, @core::array::Array::<core::felt252>() = v10, @v0 = v3, @v1 = v5, @v8 = v10, core::array::Array::<core::felt252>() = v6, core::array::Array::<core::felt252>(v0) = v7, core::array::Array::<core::felt252>(v0, v1) = v8, core::array::Span::<core::felt252>(v10) = v11, v0 = v2, v1 = v4, v10 = v12, v10 = v15, v11 = v25, v8 = v9

//! > ==========================================================================

//! > Append to unknown array then snapshot pop_back recovers appended element.

//! > TODO: Currently the analysis does not propagate through arrays with unknown initial contents.

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(mut arr: Array<felt252>) {
    arr.append(3);
    let mut span = arr.span();
    match span.pop_back() {
        Option::Some(val) => { use_snap_felt(val); },
        Option::None => {},
    };
}

//! > function_name
foo

//! > module_code
extern fn use_snap_felt(x: @felt252) nopanic;

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::array::Array::<core::felt252>
blk0 (root):
Statements:
  (v1: core::felt252) <- 3
  (v2: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v0, v1)
  (v3: core::array::Array::<core::felt252>, v4: @core::array::Array::<core::felt252>) <- snapshot(v2)
  (v5: core::array::Span::<core::felt252>) <- struct_construct(v4)
  (v6: @core::array::Array::<core::felt252>) <- struct_destructure(v5)
End:
  Match(match core::array::array_snapshot_pop_back::<core::felt252>(v6) {
    Option::Some(v7, v8) => blk1,
    Option::None(v9) => blk2,
  })

blk1:
Statements:
  (v10: @core::felt252) <- unbox(v8)
  () <- test::use_snap_felt(v10)
End:
  Return()

blk2:
Statements:
  (v11: ()) <- struct_construct()
End:
  Return()

//! > analysis_state
Block 0:
@v2 = v4, core::array::Span::<core::felt252>(v4) = v5, v2 = v3, v4 = v6

Block 1:
@v2 = v4, Box(v10) = v8, core::array::Span::<core::felt252>(v4) = v5, v2 = v3, v4 = v6

Block 2:
()() = v11, @core::array::Array::<core::felt252>() = v4, @v2 = v4, core::array::Span::<core::felt252>(v4) = v5, v2 = v3, v4 = v6, v4 = v9

//! > ==========================================================================

//! > Test pop_front None arm records array as empty

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(mut arr: Array<felt252>) -> Array<felt252> {
    match arr.pop_front() {
        Option::Some(_val) => arr,
        Option::None => {
            let empty = ArrayTrait::new();
            empty
        },
    }
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::array::Array::<core::felt252>
blk0 (root):
Statements:
End:
  Match(match core::array::array_pop_front::<core::felt252>(v0) {
    Option::Some(v1, v2) => blk1,
    Option::None(v3) => blk2,
  })

blk1:
Statements:
  (v4: core::felt252) <- unbox(v2)
End:
  Return(v1)

blk2:
Statements:
  (v5: ()) <- struct_construct()
  (v6: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
End:
  Return(v6)

//! > analysis_state
Block 0:
(empty)

Block 1:
Box(v4) = v2

Block 2:
()() = v5, core::array::Array::<core::felt252>() = v0, v0 = v3, v0 = v6

//! > ==========================================================================

//! > Test boxed enum constructs with different variants do not spuriously union inputs

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: felt252, y: felt252) {
    let a = Option::Some(x);
    let b: Option<felt252> = Option::None;
    let box_a = BoxTrait::new(a);
    let box_b = BoxTrait::new(b);
    use_boxes(box_a, box_b);
}

//! > function_name
foo

//! > module_code
extern fn use_boxes(a: Box<Option<felt252>>, b: Box<Option<felt252>>) nopanic;

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252
blk0 (root):
Statements:
  (v2: core::option::Option::<core::felt252>) <- Option::Some(v0)
  (v3: ()) <- struct_construct()
  (v4: core::option::Option::<core::felt252>) <- Option::None(v3)
  (v5: core::box::Box::<core::option::Option::<core::felt252>>) <- into_box(v2)
  (v6: core::box::Box::<core::option::Option::<core::felt252>>) <- into_box(v4)
  () <- test::use_boxes(v5, v6)
End:
  Return()

//! > analysis_state
Block 0:
()() = v3, Box(v2) = v5, Box(v4) = v6, None(v3) = v4, Some(v0) = v2