Skip to content

compare.rs test fails on contract1 and contract2 #40

@zjp-CN

Description

@zjp-CN

1214042

This is because names are considered in hashing, which some SourceCodes are different any more. (Starting from 28fdbc2 )

It means adding a unrelated proof may accidentally influence another proof. This is pretty bad.

3c3
<     "hash": "57149169904034249913882252179367046013",
---
>     "hash": "1376080800738824894316073661977482232155",
...
610c610
<           "name": "core::slice::<impl [u8]>::split_at",
---
>           "name": "core::slice::<impl [usize]>::as_chunks::<4>",
613c613
<           "src": "pub const fn split_at(&self, mid: usize) -> (&[T], &[T]) {\n        match self.split_at_checked(mid) {\n            Some(pair) => pair,\n            None => panic!(\"mid > len\"),\n        }\n    }",
---
>           "src": "pub const fn as_chunks<const N: usize>(&self) -> (&[[T; N]], &[T]) {\n        assert!(N != 0, \"chunk size must be non-zero\");\n        let len_rounded_down = self.len() / N * N;\n        // SAFETY: The rounded-down value is always the same or smaller than the\n        // original length, and thus must be in-bounds of the slice.\n        let (multiple_of_n, remainder) = unsafe { self.split_at_unchecked(len_rounded_down) };\n        // SAFETY: We already panicked for zero, and ensured by construction\n        // that the length of the subslice is a multiple of N.\n        let array_slice = unsafe { multiple_of_n.as_chunks_unchecked() };\n        (array_slice, remainder)\n    }",
618c618
<         "def_id": "DefId { id: 184, name: \"core::slice::<impl [T]>::split_at_checked\" }",
---
>         "def_id": "DefId { id: 192, name: \"core::slice::<impl [T]>::as_chunks_unchecked\" }",
620c620
<           "name": "core::slice::<impl [u8]>::split_at_checked",
---
>           "name": "core::slice::<impl [usize]>::as_chunks_unchecked::<4>",
623c623
<           "src": "pub const fn split_at_checked(&self, mid: usize) -> Option<(&[T], &[T])> {\n        if mid <= self.len() {\n            // SAFETY: `[ptr; mid]` and `[mid; len]` are inside `self`, which\n            // fulfills the requirements of `split_at_unchecked`.\n            Some(unsafe { self.split_at_unchecked(mid) })\n        } else {\n            None\n        }\n    }",
---
>           "src": "pub const unsafe fn as_chunks_unchecked<const N: usize>(&self) -> &[[T; N]] {\n        assert_unsafe_precondition!(\n            check_language_ub,\n            \"slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks\",\n            (n: usize = N, len: usize = self.len()) => n != 0 && len % n == 0,\n        );\n        // SAFETY: Caller must guarantee that `N` is nonzero and exactly divides the slice length\n        let new_len = unsafe { exact_div(self.len(), N) };\n        // SAFETY: We cast a slice of `new_len * N` elements into\n        // a slice of `new_len` many `N` elements chunks.\n        unsafe { from_raw_parts(self.as_ptr().cast(), new_len) }\n    }",
628c628
<         "def_id": "DefId { id: 171, name: \"core::slice::<impl [T]>::as_chunks\" }",
---
>         "def_id": "DefId { id: 195, name: \"core::slice::<impl [T]>::as_ptr\" }",
630c630
<           "name": "core::slice::<impl [usize]>::as_chunks::<4>",
---
>           "name": "core::slice::<impl [usize]>::as_ptr",
633c633
<           "src": "pub const fn as_chunks<const N: usize>(&self) -> (&[[T; N]], &[T]) {\n        assert!(N != 0, \"chunk size must be non-zero\");\n        let len_rounded_down = self.len() / N * N;\n        // SAFETY: The rounded-down value is always the same or smaller than the\n        // original length, and thus must be in-bounds of the slice.\n        let (multiple_of_n, remainder) = unsafe { self.split_at_unchecked(len_rounded_down) };\n        // SAFETY: We already panicked for zero, and ensured by construction\n        // that the length of the subslice is a multiple of N.\n        let array_slice = unsafe { multiple_of_n.as_chunks_unchecked() };\n        (array_slice, remainder)\n    }",
---
>           "src": "pub const fn as_ptr(&self) -> *const T {\n        self as *const [T] as *const T\n    }",
638c638
<         "def_id": "DefId { id: 197, name: \"core::slice::<impl [T]>::as_chunks_unchecked\" }",
---
>         "def_id": "DefId { id: 177, name: \"core::slice::<impl [T]>::chunks\" }",
640c640
<           "name": "core::slice::<impl [usize]>::as_chunks_unchecked::<4>",
---
>           "name": "core::slice::<impl [usize]>::chunks",
643c643
<           "src": "pub const unsafe fn as_chunks_unchecked<const N: usize>(&self) -> &[[T; N]] {\n        assert_unsafe_precondition!(\n            check_language_ub,\n            \"slice::as_chunks_unchecked requires `N != 0` and the slice to split exactly into `N`-element chunks\",\n            (n: usize = N, len: usize = self.len()) => n != 0 && len % n == 0,\n        );\n        // SAFETY: Caller must guarantee that `N` is nonzero and exactly divides the slice length\n        let new_len = unsafe { exact_div(self.len(), N) };\n        // SAFETY: We cast a slice of `new_len * N` elements into\n        // a slice of `new_len` many `N` elements chunks.\n        unsafe { from_raw_parts(self.as_ptr().cast(), new_len) }\n    }",
---
>           "src": "pub fn chunks(&self, chunk_size: usize) -> Chunks<'_, T> {\n        assert!(chunk_size != 0, \"chunk size must be non-zero\");\n        Chunks::new(self, chunk_size)\n    }",
648c648
<         "def_id": "DefId { id: 186, name: \"core::slice::<impl [T]>::as_ptr\" }",
---
>         "def_id": "DefId { id: 175, name: \"core::slice::<impl [T]>::is_empty\" }",
650c650
<           "name": "core::slice::<impl [usize]>::as_ptr",
---
>           "name": "core::slice::<impl [usize]>::is_empty",
653c653
<           "src": "pub const fn as_ptr(&self) -> *const T {\n        self as *const [T] as *const T\n    }",
---
>           "src": "pub const fn is_empty(&self) -> bool {\n        self.len() == 0\n    }",
658c658
<         "def_id": "DefId { id: 169, name: \"core::slice::<impl [T]>::chunks\" }",
---
>         "def_id": "DefId { id: 212, name: \"core::slice::<impl [T]>::split_at\" }",
660c660
<           "name": "core::slice::<impl [usize]>::chunks",
---
>           "name": "core::slice::<impl [usize]>::split_at",
663c663
<           "src": "pub fn chunks(&self, chunk_size: usize) -> Chunks<'_, T> {\n        assert!(chunk_size != 0, \"chunk size must be non-zero\");\n        Chunks::new(self, chunk_size)\n    }",
---
>           "src": "pub const fn split_at(&self, mid: usize) -> (&[T], &[T]) {\n        match self.split_at_checked(mid) {\n            Some(pair) => pair,\n            None => panic!(\"mid > len\"),\n        }\n    }",
668c668
<         "def_id": "DefId { id: 167, name: \"core::slice::<impl [T]>::is_empty\" }",
---
>         "def_id": "DefId { id: 216, name: \"core::slice::<impl [T]>::split_at_checked\" }",
670c670
<           "name": "core::slice::<impl [usize]>::is_empty",
---
>           "name": "core::slice::<impl [usize]>::split_at_checked",
673c673
<           "src": "pub const fn is_empty(&self) -> bool {\n        self.len() == 0\n    }",
---
>           "src": "pub const fn split_at_checked(&self, mid: usize) -> Option<(&[T], &[T])> {\n        if mid <= self.len() {\n            // SAFETY: `[ptr; mid]` and `[mid; len]` are inside `self`, which\n            // fulfills the requirements of `split_at_unchecked`.\n            Some(unsafe { self.split_at_unchecked(mid) })\n        } else {\n            None\n        }\n    }",
678c678
<         "def_id": "DefId { id: 185, name: \"core::slice::<impl [T]>::split_at_unchecked\" }",
---
>         "def_id": "DefId { id: 191, name: \"core::slice::<impl [T]>::split_at_unchecked\" }",
688c688
<         "def_id": "DefId { id: 172, name: \"core::slice::iter::<impl std::iter::IntoIterator for &'a [T]>::into_iter\" }",
---
>         "def_id": "DefId { id: 180, name: \"core::slice::iter::<impl std::iter::IntoIterator for &'a [T]>::into_iter\" }",
698c698
<         "def_id": "DefId { id: 163, name: \"core::str::<impl str>::as_bytes\" }",
---
>         "def_id": "DefId { id: 112, name: \"core::str::<impl str>::as_bytes\" }",

...

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions