Skip to content

fix(types): make #pointeeProjection confluent with source-first unwrapping strategy#988

Open
Stevengre wants to merge 7 commits intomasterfrom
jh/close-account-multisig-write-volatile-array
Open

fix(types): make #pointeeProjection confluent with source-first unwrapping strategy#988
Stevengre wants to merge 7 commits intomasterfrom
jh/close-account-multisig-write-volatile-array

Conversation

@Stevengre
Copy link
Contributor

@Stevengre Stevengre commented Mar 16, 2026

Summary

  • Fixes stuck execution caused by incorrect projection chains from #pointeeProjection
  • Root cause: non-deterministic overlap between struct and array rules — when source is a struct and target is an array (or vice versa), both rules match and the LLVM backend's choice determines correctness
  • Commit history shows why [priority(45)] alone doesn't work (it fixes one case but regresses the other)
  • Fix: always unwrap the source type first; target-side unwrapping deferred to #pointeeProjectionTarget
  • Reproducer from @dkcumming's review comment (minimal Wrapper([u8; 2]) cast)

Test plan

  • ptr-cast-wrapper-to-array passes (new reproducer)
  • iter_next_2 still passes (regression test for opposite overlap: [Thing;3] → Thing)
  • Full integration test suite passes

Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

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

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: beef218f11

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@Stevengre Stevengre marked this pull request as draft March 16, 2026 03:38
@Stevengre Stevengre force-pushed the jh/close-account-multisig-write-volatile-array branch 3 times, most recently from d232a5f to 72cb233 Compare March 16, 2026 05:41
@Stevengre Stevengre changed the base branch from feature/p-token to master March 16, 2026 05:41
@Stevengre Stevengre force-pushed the jh/close-account-multisig-write-volatile-array branch 3 times, most recently from 490d167 to 9afd294 Compare March 16, 2026 06:59
@Stevengre Stevengre changed the title fix(rt): normalize singleton-array volatile pubkey writes fix(rt): cancel SingletonArray+Field(0)+ConstantIndex(0) in traversal Mar 16, 2026
@Stevengre Stevengre changed the title fix(rt): cancel SingletonArray+Field(0)+ConstantIndex(0) in traversal fix(rt): handle SingletonArray+Field(0)+ConstantIndex(0) in traversal Mar 16, 2026
@Stevengre Stevengre requested review from dkcumming and mariaKt March 16, 2026 07:16
@Stevengre Stevengre marked this pull request as ready for review March 16, 2026 07:16
@Stevengre Stevengre self-assigned this Mar 16, 2026
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.

This feels like it is addressing the symptom of a problem and not the problem itself. The description given does not fill me with much confidence that the problem is being accurately understood or addressed. It feels to me the problem is the projection chain is being built incorrect, and this dismisses a particular bad projection chain. But really we want to construct correct projection chains so everything is fixed for the general case and not this particular instance of a bad chain.

I tried looking the example you provided but it adds a lot of noise, I think something like this is much better to analyse and has the same problem and everything goes wrong within the first basic block:

struct Wrapper([u8; 2]);

fn main() {
    let w = Wrapper([11, 22]);
    let arr: [u8; 2] = unsafe { *((&w) as *const Wrapper as *const [u8; 2]) };
    assert_eq!(arr, [11, 22]);
}
Image

This proof gets stuck on Node 72 (Statement: _3 <- Use(cp((*_4)))) with stuck state:

#traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ListItem (Integer ( 11 , 8 , false ))
     ListItem (Integer ( 22 , 8 , false ))
     ))
   ) , projectionElemSingletonArray  projectionElemField ( fieldIdx ( 0 ) , ty ( 80 ) )  projectionElemConstantIndex ( ... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems , .Contexts )

Which shows there is projectionElemSingletonArray then projectionElemField(0, ...) then projectionElemConstantIndex(0, ...). The first thing that comes to mind is the rules @jberthold added that should cancel the projections out types.md:65-67, but they don't apply when the projectionElemField is intersected.

// special cancellation rules with higher priority
rule maybeConcatProj(projectionElemSingletonArray, projectionElemConstantIndex(0, 0, false) REST:ProjectionElems) => REST [priority(40)]
rule maybeConcatProj(projectionElemConstantIndex(0, 0, false), projectionElemSingletonArray REST:ProjectionElems) => REST [priority(40)]

So is that field projection the problem, or are the array projections the problem? The projections are first introduced at Node 64 (Statement: _4 <- Cast-PtrToPtr mv(5)) which is the result of casting ty(81)/*const Wrapper to ty(76)/*const [u8; 2]:

#cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , castKindPtrToPtr , ty ( 81 ) , ty ( 76 ) )

giving:

PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionElemSingletonArray  projectionElemField ( fieldIdx ( 0 ) , ty ( 80 ) )  projectionElemConstantIndex ( ... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 2 ) , 0 , noMetadataSize ) )

So this looks wrong, it shouldn't have these array projections, just the field access.

This projection chain is built from data.md:1458,1469 which appends projections by #typeProjection. If you follow the logic through, what you find is that #pointeeProjection for typeInfoArrayType is being matched:

rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2)
    => maybeConcatProj(
          projectionElemConstantIndex(0, 0, false),
          #pointeeProjection(lookupTy(TY1), TY2)
        )
  rule #pointeeProjection(TY1, typeInfoArrayType(TY2, _))
    => maybeConcatProj(
          projectionElemSingletonArray,
          #pointeeProjection(TY1, lookupTy(TY2))
        )

The comment and the PR that introduces the rule #936 would indicate this is for casts of the form T -> [T; N] or [T; N] -> T, however there is no appropriate guard on the rule, or restriction for the rule to only match for casts of that case. The approach to solve this is to choose an appropriate guard (no easy I imagine because the guard will rely on context that the casts is of the form T -> [T; N] or [T; N] -> T. So problem the flow of rules needs to change.

As hacky tests I added [priority(55)] on the rules, and tried a contrived restrictive guard. Both approaches resulted in the minimised test passing, with node 64 only having the projectionFieldElem(0, ...) as expected:

 PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 80 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 2 ) , 0 , noMetadataSize ) )

I personally would change the test to be the minimised one I provided, but that is not strictly necessary. However I think any rule being suggested to solve this issue should be argued with thorough evidence that they are addressing the problem and not a symptom of the problem.

Stevengre added a commit that referenced this pull request Mar 20, 2026
Demonstrates stuck #traverseProjection caused by incorrect projection
chain SingletonArray+Field(0)+ConstantIndex(0) from #pointeeProjection
when casting *const Wrapper to *const [u8; 2].

Minimal reproducer from @dkcumming's review comment on PR #988.
@Stevengre Stevengre force-pushed the jh/close-account-multisig-write-volatile-array branch from 9afd294 to deb736c Compare March 20, 2026 09:42
@Stevengre Stevengre changed the title fix(rt): handle SingletonArray+Field(0)+ConstantIndex(0) in traversal fix(types): make #pointeeProjection confluent with source-first unwrapping strategy Mar 20, 2026
Demonstrates stuck #traverseProjection caused by incorrect projection
chain SingletonArray+Field(0)+ConstantIndex(0) from #pointeeProjection
when casting *const Wrapper to *const [u8; 2].

Minimal reproducer from @dkcumming's review comment on PR #988.
This fixes ptr-cast-wrapper-to-array by ensuring struct unwrapping
takes precedence over array unwrapping. However, it REGRESSES
iter_next_2 (renamed to iter_next_2-fail) because that test needs
the opposite priority (array first for [Thing;3] → Thing).

This commit demonstrates why priority alone cannot fix the
non-deterministic overlap — the two cases need conflicting priorities.
@Stevengre Stevengre force-pushed the jh/close-account-multisig-write-volatile-array branch from deb736c to 18334d1 Compare March 20, 2026 09:46
Revert the priority approach (which regressed iter_next_2) and instead
refactor #pointeeProjection to always unwrap the source type first.
Target-side unwrapping is deferred to #pointeeProjectionTarget, only
reached when source cannot be unwrapped further.

This eliminates the non-deterministic overlap because a type cannot be
both a struct and an array simultaneously. Both ptr-cast-wrapper-to-array
and iter_next_2 now pass.
@Stevengre Stevengre force-pushed the jh/close-account-multisig-write-volatile-array branch from 18334d1 to aeefea2 Compare March 20, 2026 09:57
Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

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

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: aeefea2a3b

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

The proof now passes with just #EndProgram, no interesting show output.
Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

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

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 0877ae1791

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

@Stevengre Stevengre marked this pull request as draft March 20, 2026 10:36
The reverse cast *const [u8; 2] → *const Wrapper([u8; 2]) gets stuck
on both master and with the source-first strategy. This is a
pre-existing limitation of #pointeeProjection: source-first unwraps
the array before considering the target struct, producing an
uncancelable SingletonArray in the projection chain.
When source is an array and target is a transparent struct wrapping
that same array type (e.g., *const [u8;2] → *const Wrapper([u8;2])),
the source-first strategy incorrectly unwraps the array first,
producing an uncancelable SingletonArray in the projection chain.

Add a prioritized rule that detects this case (lookupTy(FIELD) ==K SRC)
and directly produces WrapStruct, deferring to target-side wrapping.

The expected output for ptr-cast-array-to-wrapper-fail now shows
node 7 reaching #EndProgram (was previously stuck on
#traverseProjection). The test still fails overall due to an
unrelated alignment assertion on the other proof branch.
@Stevengre Stevengre marked this pull request as ready for review March 20, 2026 11:51
@Stevengre Stevengre requested a review from dkcumming March 20, 2026 11:51
Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

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

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: c22c881c74

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

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.

3 participants