Skip to content

Commit 61b6c6b

Browse files
StevengreStevengre
committed
feat: trying to close the implementation
1 parent 9cc4eb2 commit 61b6c6b

File tree

2 files changed

+130
-87
lines changed

2 files changed

+130
-87
lines changed

‎kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md‎

Lines changed: 124 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -20,40 +20,41 @@ module KMIR-SPL-TOKEN
2020
## Helper syntax
2121

2222
```k
23-
syntax Value ::= SPLRefCellData ( Value )
24-
| SPLRefCellLamports ( U64 )
23+
syntax Value ::= SPLRc ( Value ) // work as reference to data and lamports
24+
| SPLRefCell ( Value )
2525
| SPLDataBuffer ( Value )
2626
| SPLDataBorrow ( Place , Value )
2727
| SPLDataBorrowMut ( Place , Value )
2828
```
2929

30-
## Cheatcode handling
3130

31+
## Cheatcode handling
3232
```{.k .symbolic}
3333
rule [cheatcode-is-spl-account]:
3434
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
3535
=> #setLocalValue(
3636
place(LOCAL, appendP(PROJS, projectionElemDeref .ProjectionElems)),
3737
Aggregate(variantIdx(0),
38-
ListItem(Range(?SplAccountKey:List))
39-
ListItem(SPLRefCellLamports(U64(?SplLamports:Int)))
40-
ListItem(SPLRefCellData(SPLDataBuffer(
38+
ListItem(Range(?SplAccountKey:List)) // pub key: &'a Pubkey
39+
ListItem(SPLRc(SPLRefCell(Integer(?SplLamports:Int, 64, false)))) // lamports: Rc<RefCell<&'a mut u64>>
40+
ListItem(Aggregate(variantIdx(0), ListItem( Aggregate(variantIdx(0), ListItem( // data: Rc<RefCell<&'a mut [u8]>>
41+
SPLRc(SPLRefCell(SPLDataBuffer( // data: Rc<RefCell<&'a mut [u8]>>, Aggregate is for &account.data
4142
Aggregate(variantIdx(0),
42-
ListItem(Range(?SplMintKey:List))
43-
ListItem(Range(?SplTokenOwnerKey:List))
44-
ListItem(Integer(?SplAmount:Int, 64, false))
45-
ListItem(?SplDelegateCOpt:Value)
46-
ListItem(Integer(?SplAccountState:Int, 8, false))
47-
ListItem(?SplIsNativeCOpt:Value)
48-
ListItem(Integer(?SplDelegatedAmount:Int, 64, false))
49-
ListItem(?SplCloseAuthCOpt:Value)
43+
ListItem(Range(?SplMintKey:List)) // Account.mint: Pubkey
44+
ListItem(Range(?SplTokenOwnerKey:List)) // Account.owner: Pubkey
45+
ListItem(Integer(?SplAmount:Int, 64, false)) // Account.amount: u64
46+
ListItem(?SplDelegateCOpt:Value) // Account.delegate: COption<Pubkey>
47+
ListItem(Integer(?SplAccountState:Int, 8, false)) // Account.state: AccountState (repr u8)
48+
ListItem(?SplIsNativeCOpt:Value) // Account.is_native: COption<u64>
49+
ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64
50+
ListItem(?SplCloseAuthCOpt:Value) // Account.close_authority: COption<Pubkey>
5051
)
51-
)))
52-
ListItem(Range(?SplOwnerKey))
53-
ListItem(Integer(?SplRentEpoch:Int, 64, false))
54-
ListItem(BoolVal(?_SplIsSigner:Bool))
55-
ListItem(BoolVal(?_SplIsWritable:Bool))
56-
ListItem(BoolVal(?_SplExecutable:Bool))
52+
))))))))
53+
ListItem(Range(?SplOwnerKey)) // owner: &'a Pubkey
54+
ListItem(Integer(?SplRentEpoch:Int, 64, false)) // rent_epoch: u64
55+
ListItem(BoolVal(?_SplIsSigner:Bool)) // is_signer: bool
56+
ListItem(BoolVal(?_SplIsWritable:Bool)) // is_writable: bool
57+
ListItem(BoolVal(?_SplExecutable:Bool)) // executable: bool
5758
)
5859
)
5960
~> #execBlockIdx(TARGET)
@@ -94,93 +95,134 @@ module KMIR-SPL-TOKEN
9495
[priority(30), preserves-definedness]
9596
```
9697

97-
## RefCell::<&mut [u8]> helpers
98+
## Accessing `Rc<RefCell<_>>`
99+
98100

99101
```k
100-
rule [spl-borrow-data]:
101-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
102-
=> #mkSPLBorrowData(DEST, operandCopy(place(LOCAL, PROJS)), place(LOCAL, PROJS), false)
103-
~> #execBlockIdx(TARGET)
104-
...
105-
</k>
106-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "core::cell::RefCell::<&mut [u8]>::borrow"
107-
[priority(30), preserves-definedness]
102+
rule <k> #cast(SPLRc(VALUE), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
103+
=> SPLRc(VALUE) ...
104+
</k>
105+
requires #typesCompatible(lookupTy(TY_SOURCE), lookupTy(TY_TARGET))
106+
[preserves-definedness] // valid map lookups checked
107+
```
108108

109-
rule [spl-borrow-mut-data]:
110-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
111-
=> #mkSPLBorrowData(DEST, operandCopy(place(LOCAL, PROJS)), place(LOCAL, PROJS), true)
112-
~> #execBlockIdx(TARGET)
109+
We shortcut the MIR field access that `<Rc<_> as Deref>::deref` performs and
110+
expose the wrapped payload directly.
111+
112+
```k
113+
rule <k> #traverseProjection(
114+
DEST,
115+
SPLRc(VALUE),
116+
projectionElemDeref PROJS,
117+
CTXTS
118+
)
119+
=> #traverseProjection(
120+
DEST,
121+
VALUE,
122+
PROJS,
123+
CtxSPLRc CTXTS
124+
)
125+
...
126+
</k>
127+
[priority(30)]
128+
129+
syntax Context ::= "CtxSPLRc"
130+
131+
rule #buildUpdate(VAL, CtxSPLRc CTXS) => #buildUpdate(SPLRc(VAL), CTXS)
132+
rule #projectionsFor(CtxSPLRc CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)
133+
134+
rule [spl-rc-deref]:
135+
<k> #execTerminator(
136+
terminator(
137+
terminatorKindCall(FUNC, OP:Operand OPS:Operands, DEST, TARGET, UNWIND),
138+
_SPAN))
139+
=> #finishSPLRcDeref(OP, DEST, TARGET, FUNC, OP OPS, UNWIND)
113140
...
114141
</k>
115-
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "core::cell::RefCell::<&mut [u8]>::borrow_mut"
142+
requires #functionName(lookupFunction(#tyOfCall(FUNC)))
143+
==String "<std::rc::Rc<std::cell::RefCell<std::vec::Vec<u8>>> as std::ops::Deref>::deref"
116144
[priority(30), preserves-definedness]
117145
118-
syntax KItem ::= #mkSPLBorrowData ( Place , Evaluation , Place , Bool ) [seqstrict(2)]
146+
syntax KItem ::= #finishSPLRcDeref ( Evaluation , Place , MaybeBasicBlockIdx , Operand , Operands , UnwindAction ) [seqstrict(1)]
147+
148+
// rule <k> #finishSPLRcDeref(SPLRc(VALUE), DEST, TARGET, _FUNC, _ARGS, _UNWIND)
149+
// => #setLocalValue(DEST, VALUE) ~> #continueAt(TARGET)
150+
// ...
151+
// </k>
152+
153+
// rule [spl-rc-deref-fallback]:
154+
// <k> #finishSPLRcDeref(_VAL:Value, DEST, TARGET, FUNC, ARGS, UNWIND)
155+
// => #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS)
156+
// ...
157+
// </k>
158+
// <currentFunc> CALLER => #tyOfCall(FUNC) </currentFunc>
159+
// <currentFrame>
160+
// <currentBody> _ </currentBody>
161+
// <caller> OLDCALLER => CALLER </caller>
162+
// <dest> OLDDEST => DEST </dest>
163+
// <target> OLDTARGET => TARGET </target>
164+
// <unwind> OLDUNWIND => UNWIND </unwind>
165+
// <locals> LOCALS </locals>
166+
// </currentFrame>
167+
// <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
168+
// [owise]
169+
```
119170

120-
rule <k> #mkSPLBorrowData(DEST, SPLRefCellData(BUF), SRC, false)
121-
=> #setLocalValue(DEST, SPLDataBorrow(SRC, BUF))
171+
```k
172+
rule <k> #traverseProjection(
173+
DEST,
174+
SPLRefCell(VALUE),
175+
projectionElemField(fieldIdx(2), TY) PROJS,
176+
CTXTS
177+
)
178+
=> #traverseProjection(
179+
DEST,
180+
VALUE,
181+
PROJS,
182+
CtxSPLRefCell(TY) CTXTS
183+
)
122184
...
123-
</k>
185+
</k>
186+
[priority(30)]
124187
125-
rule <k> #mkSPLBorrowData(DEST, SPLRefCellData(BUF), SRC, true)
126-
=> #setLocalValue(DEST, SPLDataBorrowMut(SRC, BUF))
127-
...
128-
</k>
188+
syntax Context ::= CtxSPLRefCell ( Ty )
189+
190+
rule #buildUpdate(VAL, CtxSPLRefCell(_) CTXS) => #buildUpdate(SPLRefCell(VAL), CTXS)
191+
rule #projectionsFor(CtxSPLRefCell(TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(fieldIdx(2), TY) PROJS)
129192
```
130193

131-
## Account::unpack / Account::pack
194+
## RefCell::<&mut [u8]> helpers
132195

133196
```k
134-
rule [spl-account-unpack]:
135-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(ARG) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
136-
=> #mkSPLAccountUnpack(DEST, operandCopy(ARG))
197+
rule [spl-borrow-data]:
198+
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
199+
=> #mkSPLBorrowData(DEST, operandCopy(place(LOCAL, PROJS)), place(LOCAL, PROJS), false)
137200
~> #execBlockIdx(TARGET)
138201
...
139202
</k>
140-
requires (
141-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::state::Account::unpack_unchecked"
142-
orBool
143-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::state::Account::unpack"
144-
orBool
145-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "Account::unpack_unchecked"
146-
)
203+
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "std::cell::RefCell::<std::vec::Vec<u8>>::borrow"
147204
[priority(30), preserves-definedness]
148205
149-
syntax KItem ::= #mkSPLAccountUnpack ( Place , Evaluation ) [seqstrict(2)]
150-
151-
rule <k> #mkSPLAccountUnpack(DEST, SPLDataBorrow(_, SPLDataBuffer(ACCOUNT)))
152-
=> #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(ACCOUNT)))
153-
...
154-
</k>
155-
156-
rule <k> #mkSPLAccountUnpack(DEST, SPLDataBorrowMut(_, SPLDataBuffer(ACCOUNT)))
157-
=> #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(ACCOUNT)))
158-
...
159-
</k>
160-
161-
rule [spl-account-pack]:
162-
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(SRC) operandCopy(BUF) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
163-
=> #mkSPLAccountPack(operandCopy(SRC), operandCopy(BUF), DEST)
206+
rule [spl-borrow-mut-data]:
207+
<k> #execTerminator(terminator(terminatorKindCall(FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
208+
=> #mkSPLBorrowData(DEST, operandCopy(place(LOCAL, PROJS)), place(LOCAL, PROJS), true)
164209
~> #execBlockIdx(TARGET)
165210
...
166211
</k>
167-
requires (
168-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "spl_token::state::Account::pack"
169-
orBool
170-
#functionName(lookupFunction(#tyOfCall(FUNC))) ==String "Account::pack"
171-
)
212+
requires #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "std::cell::RefCell::<std::vec::Vec<u8>>::borrow_mut"
172213
[priority(30), preserves-definedness]
173214
174-
syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation , Place ) [seqstrict(2)]
215+
syntax KItem ::= #mkSPLBorrowData ( Place , Evaluation , Place , Bool ) [seqstrict(2)]
175216
176-
rule <k> #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_)), DEST)
177-
=> #setLocalValue(
178-
PLACE,
179-
SPLRefCellData(SPLDataBuffer(ACCOUNT))
180-
)
181-
~> #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List))))
182-
...
183-
</k>
217+
// rule <k> #mkSPLBorrowData(DEST, SPLRefCellData(BUF), SRC, false)
218+
// => #setLocalValue(DEST, SPLDataBorrow(SRC, BUF))
219+
// ...
220+
// </k>
221+
222+
// rule <k> #mkSPLBorrowData(DEST, SPLRefCellData(BUF), SRC, true)
223+
// => #setLocalValue(DEST, SPLDataBorrowMut(SRC, BUF))
224+
// ...
225+
// </k>
184226
```
185227

186228
```k

‎kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -41,14 +41,15 @@ impl AccountInfo {
4141

4242
fn test_spltoken_domain_data(acc: &AccountInfo, _mint: &AccountInfo, _rent: &AccountInfo) {
4343
cheatcode_is_spl_account(acc);
44+
let x = &acc.data.borrow();
4445

45-
let mut account = Account::unpack_unchecked(&acc.data.borrow()).unwrap();
46+
// let mut account = Account::unpack_unchecked(&acc.data.borrow()).unwrap();
4647

47-
account.is_native = COption::Some(0);
48-
Account::pack(account, &mut acc.data.borrow_mut()[..]).unwrap();
48+
// account.is_native = COption::Some(0);
49+
// Account::pack(account, &mut acc.data.borrow_mut()[..]).unwrap();
4950

50-
let unpacked = get_account(acc);
51-
assert!(unpacked.is_native());
51+
// let unpacked = get_account(acc);
52+
// assert!(unpacked.is_native());
5253
}
5354

5455
fn get_account(acc: &AccountInfo) -> Account {

0 commit comments

Comments
 (0)