//! > 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:
(empty)

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

//! > 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 array 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, v1] = v4, core::array::Array::<core::felt252>[v0] = v3

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

//! > Test long arrays keep bounded suffix tracking

//! > test_runner_name
test_equality_analysis

//! > comments
Only the last MAX_ARRAY_TRACKED_ITEMS elements stay individually tracked; everything before
them is forgotten into a placeholder prefix (rendered `?(*)`).

//! > function_code
fn foo(
    a0: felt252, a1: felt252, a2: felt252, a3: felt252, a4: felt252, a5: felt252, a6: felt252,
) -> Array<felt252> {
    let mut arr = ArrayTrait::new();
    arr.append(a0);
    arr.append(a1);
    arr.append(a2);
    arr.append(a3);
    arr.append(a4);
    arr.append(a5);
    arr.append(a6);
    arr
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252, v2: core::felt252, v3: core::felt252, v4: core::felt252, v5: core::felt252, v6: core::felt252
blk0 (root):
Statements:
  (v7: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
  (v8: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v7, v0)
  (v9: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v8, v1)
  (v10: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v9, v2)
  (v11: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v10, v3)
  (v12: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v11, v4)
  (v13: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v12, v5)
  (v14: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v13, v6)
End:
  Return(v14)

//! > analysis_state
Block 0:
core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v13, core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v6] = v14, core::array::Array::<core::felt252>[] = v7, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v12, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v11, core::array::Array::<core::felt252>[v0, v1, v2] = v10, core::array::Array::<core::felt252>[v0, v1] = v9, core::array::Array::<core::felt252>[v0] = v8

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

//! > Test pop_front on a long array with a forgotten prefix

//! > test_runner_name
test_equality_analysis

//! > comments
The popped element comes off the forgotten prefix, so its value is unknown; the remainder
stays tracked under a fresh prefix.

//! > function_code
fn foo(
    a0: felt252, a1: felt252, a2: felt252, a3: felt252, a4: felt252, a5: felt252, a6: felt252,
) -> felt252 {
    let mut arr = ArrayTrait::new();
    arr.append(a0);
    arr.append(a1);
    arr.append(a2);
    arr.append(a3);
    arr.append(a4);
    arr.append(a5);
    arr.append(a6);
    match arr.pop_front() {
        Some(x) => x,
        None => 0,
    }
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

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

blk1:
Statements:
  (v18: core::felt252) <- unbox(v16)
End:
  Return(v18)

blk2:
Statements:
  (v19: ()) <- struct_construct()
  (v20: core::felt252) <- 0
End:
  Return(v20)

//! > analysis_state
Block 0:
core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v13, core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v6] = v14, core::array::Array::<core::felt252>[] = v7, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v12, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v11, core::array::Array::<core::felt252>[v0, v1, v2] = v10, core::array::Array::<core::felt252>[v0, v1] = v9, core::array::Array::<core::felt252>[v0] = v8

Block 1:
Box(v18) = v16, core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v13, core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v6] = v14, core::array::Array::<core::felt252>[?(*), v3, v4, v5, v6] = v15, core::array::Array::<core::felt252>[] = v7, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v12, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v11, core::array::Array::<core::felt252>[v0, v1, v2] = v10, core::array::Array::<core::felt252>[v0, v1] = v9, core::array::Array::<core::felt252>[v0] = v8

Block 2:
()() = v19, core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v13, core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v6] = v14, core::array::Array::<core::felt252>[] = v7, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v12, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v11, core::array::Array::<core::felt252>[v0, v1, v2] = v10, core::array::Array::<core::felt252>[v0, v1] = v9, core::array::Array::<core::felt252>[v0] = v8

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

//! > Test long arrays merge across branches keeping suffix elements

//! > test_runner_name
test_equality_analysis

//! > comments
Both branches build the same 7-element array, whose forgotten prefix has a branch-local
placeholder; the merge keeps the shared suffix elements under a fresh placeholder, and the
post-merge append extends the merged relation.

//! > function_code
fn foo(
    a0: felt252,
    a1: felt252,
    a2: felt252,
    a3: felt252,
    a4: felt252,
    a5: felt252,
    a6: felt252,
    a7: felt252,
    c: bool,
) -> Array<felt252> {
    let mut arr = ArrayTrait::new();
    if c {
        arr.append(a0);
        arr.append(a1);
        arr.append(a2);
        arr.append(a3);
        arr.append(a4);
        arr.append(a5);
        arr.append(a6);
    } else {
        arr.append(a0);
        arr.append(a1);
        arr.append(a2);
        arr.append(a3);
        arr.append(a4);
        arr.append(a5);
        arr.append(a6);
    }
    arr.append(a7);
    arr
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252, v2: core::felt252, v3: core::felt252, v4: core::felt252, v5: core::felt252, v6: core::felt252, v7: core::felt252, v8: core::bool
blk0 (root):
Statements:
  (v9: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
End:
  Match(match_enum(v8) {
    bool::False(v10) => blk1,
    bool::True(v11) => blk2,
  })

blk1:
Statements:
  (v12: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v9, v0)
  (v13: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v12, v1)
  (v14: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v13, v2)
  (v15: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v14, v3)
  (v16: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v15, v4)
  (v17: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v16, v5)
  (v18: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v17, v6)
End:
  Goto(blk3, {v18 -> v19})

blk2:
Statements:
  (v20: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v9, v0)
  (v21: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v20, v1)
  (v22: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v21, v2)
  (v23: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v22, v3)
  (v24: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v23, v4)
  (v25: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v24, v5)
  (v26: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v25, v6)
End:
  Goto(blk3, {v26 -> v19})

blk3:
Statements:
  (v27: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v19, v7)
End:
  Return(v27)

//! > analysis_state
Block 0:
core::array::Array::<core::felt252>[] = v9

Block 1:
False(v10) = v8, core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v17, core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v6] = v18, core::array::Array::<core::felt252>[] = v9, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v16, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v15, core::array::Array::<core::felt252>[v0, v1, v2] = v14, core::array::Array::<core::felt252>[v0, v1] = v13, core::array::Array::<core::felt252>[v0] = v12

Block 2:
True(v11) = v8, core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v25, core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v6] = v26, core::array::Array::<core::felt252>[] = v9, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v24, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v23, core::array::Array::<core::felt252>[v0, v1, v2] = v22, core::array::Array::<core::felt252>[v0, v1] = v21, core::array::Array::<core::felt252>[v0] = v20

Block 3:
core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v6] = v19, core::array::Array::<core::felt252>[?(*), v3, v4, v5, v6, v7] = v27, core::array::Array::<core::felt252>[] = v9

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

//! > 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
#[allow(extern_outside_corelib)]
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, v1] = v4, core::array::Array::<core::felt252>[v0] = v3

Block 1:
Box(v0) = v6, core::array::Array::<core::felt252>[] = v2, core::array::Array::<core::felt252>[v0, v1] = v4, core::array::Array::<core::felt252>[v0] = v3, 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, v1] = v4, core::array::Array::<core::felt252>[v0] = v3

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

Block 4:
core::array::Array::<core::felt252>[] = v2, core::array::Array::<core::felt252>[v0, v1] = v4, core::array::Array::<core::felt252>[v0] = v3, 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, v1] = v4, core::array::Array::<core::felt252>[v0] = v3, v10 = v13

Block 6:
@v16 = v18, core::array::Array::<core::felt252>[] = v2, core::array::Array::<core::felt252>[v0, v1] = v4, core::array::Array::<core::felt252>[v0] = v3, 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
#[allow(extern_outside_corelib)]
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, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, 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, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, 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, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, 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>[v1] = v13, @v0 = v3, @v1 = v5, @v8 = v10, Box(v3) = v14, core::array::Array::<core::felt252>[] = v6, core::array::Array::<core::felt252>[v0, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, 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 4:
()() = v24, @v0 = v3, @v1 = v5, @v8 = v10, core::array::Array::<core::felt252>[] = v6, core::array::Array::<core::felt252>[v0, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, core::array::Span::<core::felt252>(v10) = v11, core::array::Span::<core::felt252>(v15) = v25, v0 = v2, v1 = v4, v10 = v12, 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
#[allow(extern_outside_corelib)]
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, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, 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, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, 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, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, 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>[v0] = v13, @v0 = v3, @v1 = v5, @v8 = v10, Box(v5) = v14, core::array::Array::<core::felt252>[] = v6, core::array::Array::<core::felt252>[v0, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, 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 4:
()() = v24, @v0 = v3, @v1 = v5, @v8 = v10, core::array::Array::<core::felt252>[] = v6, core::array::Array::<core::felt252>[v0, v1] = v8, core::array::Array::<core::felt252>[v0] = v7, core::array::Span::<core::felt252>(v10) = v11, core::array::Span::<core::felt252>(v15) = v25, v0 = v2, v1 = v4, v10 = v12, 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
#[allow(extern_outside_corelib)]
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, @v2 = v4, core::array::Span::<core::felt252>(v4) = v5, v2 = v3, v4 = v6

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

//! > Test arrays merge across branches with different lengths

//! > test_runner_name
test_equality_analysis

//! > comments
The branches build arrays of different lengths (sharing their trailing elements); the
common trailing elements survive the merge behind a fresh forgotten prefix.

//! > function_code
fn foo(a0: felt252, a1: felt252, a2: felt252, a3: felt252, c: bool) -> Array<felt252> {
    let mut arr = ArrayTrait::new();
    if c {
        arr.append(a1);
        arr.append(a2);
    } else {
        arr.append(a0);
        arr.append(a1);
        arr.append(a2);
    }
    arr.append(a3);
    arr
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

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

blk1:
Statements:
  (v8: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v5, v0)
  (v9: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v8, v1)
  (v10: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v9, v2)
End:
  Goto(blk3, {v10 -> v11})

blk2:
Statements:
  (v12: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v5, v1)
  (v13: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v12, v2)
End:
  Goto(blk3, {v13 -> v11})

blk3:
Statements:
  (v14: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v11, v3)
End:
  Return(v14)

//! > analysis_state
Block 0:
core::array::Array::<core::felt252>[] = v5

Block 1:
False(v6) = v4, core::array::Array::<core::felt252>[] = v5, core::array::Array::<core::felt252>[v0, v1, v2] = v10, core::array::Array::<core::felt252>[v0, v1] = v9, core::array::Array::<core::felt252>[v0] = v8

Block 2:
True(v7) = v4, core::array::Array::<core::felt252>[] = v5, core::array::Array::<core::felt252>[v1, v2] = v13, core::array::Array::<core::felt252>[v1] = v12

Block 3:
core::array::Array::<core::felt252>[?(*), v1, v2, v3] = v14, core::array::Array::<core::felt252>[?(*), v1, v2] = v11, core::array::Array::<core::felt252>[] = v5

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

//! > Test arrays merge across branches with mixed prefix presence

//! > test_runner_name
test_equality_analysis

//! > comments
One branch's array has a forgotten prefix while the other's is fully known (sharing the
trailing elements); all the common trailing elements survive the merge behind a fresh,
possibly-empty forgotten prefix.

//! > function_code
fn foo(
    a0: felt252,
    a1: felt252,
    a2: felt252,
    a3: felt252,
    a4: felt252,
    a5: felt252,
    a6: felt252,
    c: bool,
) -> Array<felt252> {
    let mut arr = ArrayTrait::new();
    if c {
        arr.append(a0);
        arr.append(a1);
        arr.append(a2);
        arr.append(a3);
        arr.append(a4);
        arr.append(a5);
    } else {
        arr.append(a1);
        arr.append(a2);
        arr.append(a3);
        arr.append(a4);
        arr.append(a5);
    }
    arr.append(a6);
    arr
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

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

blk1:
Statements:
  (v11: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v8, v1)
  (v12: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v11, v2)
  (v13: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v12, v3)
  (v14: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v13, v4)
  (v15: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v14, v5)
End:
  Goto(blk3, {v15 -> v16})

blk2:
Statements:
  (v17: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v8, v0)
  (v18: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v17, v1)
  (v19: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v18, v2)
  (v20: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v19, v3)
  (v21: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v20, v4)
  (v22: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v21, v5)
End:
  Goto(blk3, {v22 -> v16})

blk3:
Statements:
  (v23: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v16, v6)
End:
  Return(v23)

//! > analysis_state
Block 0:
core::array::Array::<core::felt252>[] = v8

Block 1:
False(v9) = v7, core::array::Array::<core::felt252>[] = v8, core::array::Array::<core::felt252>[v1, v2, v3, v4, v5] = v15, core::array::Array::<core::felt252>[v1, v2, v3, v4] = v14, core::array::Array::<core::felt252>[v1, v2, v3] = v13, core::array::Array::<core::felt252>[v1, v2] = v12, core::array::Array::<core::felt252>[v1] = v11

Block 2:
True(v10) = v7, core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v22, core::array::Array::<core::felt252>[] = v8, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v21, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v20, core::array::Array::<core::felt252>[v0, v1, v2] = v19, core::array::Array::<core::felt252>[v0, v1] = v18, core::array::Array::<core::felt252>[v0] = v17

Block 3:
core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v16, core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v6] = v23, core::array::Array::<core::felt252>[] = v8

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

//! > Test forgotten prefix is preserved across unrelated branches

//! > test_runner_name
test_equality_analysis

//! > comments
The array is built before the branch and untouched by it, so both arms reach the merge with
the same placeholder and the relation survives intact.

//! > function_code
fn foo(
    a0: felt252,
    a1: felt252,
    a2: felt252,
    a3: felt252,
    a4: felt252,
    a5: felt252,
    a6: felt252,
    c: bool,
) -> Array<felt252> {
    let mut arr = ArrayTrait::new();
    arr.append(a0);
    arr.append(a1);
    arr.append(a2);
    arr.append(a3);
    arr.append(a4);
    arr.append(a5);
    let x = if c {
        a6 + a0
    } else {
        a6 - a0
    };
    arr.append(x);
    arr
}

//! > function_name
foo

//! > module_code

//! > semantic_diagnostics

//! > lowering
Parameters: v0: core::felt252, v1: core::felt252, v2: core::felt252, v3: core::felt252, v4: core::felt252, v5: core::felt252, v6: core::felt252, v7: core::bool
blk0 (root):
Statements:
  (v8: core::array::Array::<core::felt252>) <- core::array::array_new::<core::felt252>()
  (v9: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v8, v0)
  (v10: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v9, v1)
  (v11: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v10, v2)
  (v12: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v11, v3)
  (v13: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v12, v4)
  (v14: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v13, v5)
End:
  Match(match_enum(v7) {
    bool::False(v15) => blk1,
    bool::True(v16) => blk2,
  })

blk1:
Statements:
  (v17: core::felt252) <- core::felt252_sub(v6, v0)
End:
  Goto(blk3, {v17 -> v18})

blk2:
Statements:
  (v19: core::felt252) <- core::felt252_add(v6, v0)
End:
  Goto(blk3, {v19 -> v18})

blk3:
Statements:
  (v20: core::array::Array::<core::felt252>) <- core::array::array_append::<core::felt252>(v14, v18)
End:
  Return(v20)

//! > analysis_state
Block 0:
core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v14, core::array::Array::<core::felt252>[] = v8, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v13, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v12, core::array::Array::<core::felt252>[v0, v1, v2] = v11, core::array::Array::<core::felt252>[v0, v1] = v10, core::array::Array::<core::felt252>[v0] = v9

Block 1:
False(v15) = v7, core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v14, core::array::Array::<core::felt252>[] = v8, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v13, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v12, core::array::Array::<core::felt252>[v0, v1, v2] = v11, core::array::Array::<core::felt252>[v0, v1] = v10, core::array::Array::<core::felt252>[v0] = v9

Block 2:
True(v16) = v7, core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v14, core::array::Array::<core::felt252>[] = v8, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v13, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v12, core::array::Array::<core::felt252>[v0, v1, v2] = v11, core::array::Array::<core::felt252>[v0, v1] = v10, core::array::Array::<core::felt252>[v0] = v9

Block 3:
core::array::Array::<core::felt252>[?(*), v1, v2, v3, v4, v5] = v14, core::array::Array::<core::felt252>[?(*), v2, v3, v4, v5, v18] = v20, core::array::Array::<core::felt252>[] = v8, core::array::Array::<core::felt252>[v0, v1, v2, v3, v4] = v13, core::array::Array::<core::felt252>[v0, v1, v2, v3] = v12, core::array::Array::<core::felt252>[v0, v1, v2] = v11, core::array::Array::<core::felt252>[v0, v1] = v10, core::array::Array::<core::felt252>[v0] = v9

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

//! > Test pop_front None arm does not backedge-merge or record empty on match input

//! > 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>[] = 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
#[allow(extern_outside_corelib)]
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

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

//! > Test struct construct with shared first field but different second field across branches

//! > test_runner_name
test_equality_analysis

//! > function_code
fn foo(x: @Array<felt252>, cond: bool) {
    let s = if cond {
        MyStruct { a: x, b: 1 }
    } else {
        MyStruct { a: x, b: 2 }
    };
    use_struct(@s);
}

//! > function_name
foo

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

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

//! > semantic_diagnostics

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

blk1:
Statements:
  (v4: core::felt252) <- 2
  (v5: test::MyStruct) <- struct_construct(v0, v4)
End:
  Goto(blk3, {v5 -> v6})

blk2:
Statements:
  (v7: core::felt252) <- 1
  (v8: test::MyStruct) <- struct_construct(v0, v7)
End:
  Goto(blk3, {v8 -> v6})

blk3:
Statements:
  (v9: test::MyStruct, v10: @test::MyStruct) <- snapshot(v6)
  () <- test::use_struct(v10)
End:
  Return()

//! > analysis_state
Block 0:
(empty)

Block 1:
False(v2) = v1, test::MyStruct(v0, v4) = v5

Block 2:
True(v3) = v1, test::MyStruct(v0, v7) = v8

Block 3:
@v6 = v10, test::MyStruct(v0, ?) = v6, v6 = v9
