Skip to content

Conversation

jberthold
Copy link
Member

  • Aggregate kind RawPtr (RValue) takes two arguments, a pointer and metadata, and creates a new pointer.
    No test program (yet).
  • Subslice (ProjectionElem) : operates on arrays and slices, extracts a shorter (possibly empty) slice.
    Tested using a small program that matches the tail of a slice using let [a, b, c, rest @ ..] = input_slice.

Both are required for the P-token proofs to progress.

Also copied the description of all projections from the docs into the actual semantics.

@jberthold jberthold marked this pull request as ready for review August 8, 2025 04:47
Copy link
Collaborator

@dkcumming dkcumming left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

@jberthold
Copy link
Member Author

I'll add a test later. This program from @dkcumming contains the construct but uses features we don't support yet.

use std::slice::from_raw_parts;
fn main() {
    let mut arr = [0;3];
    arr[1] = 1;
    let arr2 = unsafe { from_raw_parts((&arr).as_ptr().add(1), 2) };
    assert!(arr2[0] == arr[1]);
    assert!(arr2.len() == 2);
}

@jberthold jberthold merged commit ff9d9a6 into master Aug 8, 2025
5 checks passed
@jberthold jberthold deleted the implement-more-p-token-relevant-things branch August 8, 2025 07:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants