@@ -280,6 +280,31 @@ RefCell<&mut [u8]>
280280```
281281The ` #initBorrow ` helper resets borrow counters to 0 and sets the correct dynamicSize.
282282
283+ ``` k
284+ // #initBorrow(RefCell, N) - Initialize RefCell borrow metadata with correct buffer size
285+ // RefCell<&mut [u8]> layout:
286+ // field 0: BorrowFlag (Cell<isize>) - borrow state counter
287+ // field 1: borrow count (for runtime borrow checking)
288+ // field 2: UnsafeCell<&mut [u8]> containing the actual reference with metadata
289+ // This rule:
290+ // 1. Resets borrow counters to 0 (no active borrows)
291+ // 2. Sets the dynamicSize in metadata to N (the known buffer length: 165/82/17)
292+ syntax Evaluation ::= #initBorrow(Evaluation, Int) [seqstrict(1)]
293+ rule <k> #initBorrow(Aggregate ( variantIdx ( 0 ) ,
294+ ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) // borrow flag
295+ ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) // borrow count
296+ ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , true )))))) // inner wrapper
297+ ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( _ ) , 0 , dynamicSize ( _ )))))))) // &mut [u8] reference
298+ ), N)
299+ => Aggregate ( variantIdx ( 0 ) ,
300+ ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) // reset borrow flag to 0
301+ ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) // reset borrow count to 0
302+ ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , true ))))))
303+ ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( N ) , 0 , dynamicSize ( N )))))))) // set size to N
304+ ) ...
305+ </k>
306+ ```
307+
283308``` {.k .symbolic}
284309 // Projection path constants for navigating AccountInfo structure
285310 // Path to the actual data buffer: AccountInfo -> data -> Rc -> RcInner -> RefCell -> UnsafeCell -> &mut [u8] -> [u8]
@@ -348,29 +373,6 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
348373 andBool #isSplPubkey(?SplCloseAuthKey)
349374 [priority(30), preserves-definedness]
350375
351- // #initBorrow(RefCell, N) - Initialize RefCell borrow metadata with correct buffer size
352- // RefCell<&mut [u8]> layout:
353- // field 0: BorrowFlag (Cell<isize>) - borrow state counter
354- // field 1: borrow count (for runtime borrow checking)
355- // field 2: UnsafeCell<&mut [u8]> containing the actual reference with metadata
356- // This rule:
357- // 1. Resets borrow counters to 0 (no active borrows)
358- // 2. Sets the dynamicSize in metadata to N (the known buffer length: 165/82/17)
359- syntax Evaluation ::= #initBorrow(Evaluation, Int) [seqstrict(1)]
360- rule <k> #initBorrow(Aggregate ( variantIdx ( 0 ) ,
361- ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) // borrow flag
362- ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , false )))))) // borrow count
363- ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( _ , 64 , true )))))) // inner wrapper
364- ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( _ ) , 0 , dynamicSize ( _ )))))))) // &mut [u8] reference
365- ), N)
366- => Aggregate ( variantIdx ( 0 ) ,
367- ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) // reset borrow flag to 0
368- ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , false )))))) // reset borrow count to 0
369- ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( 0 , 64 , true ))))))
370- ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( OFFSET , PLACE , MUT , metadata ( dynamicSize ( N ) , 0 , dynamicSize ( N )))))))) // set size to N
371- ) ...
372- </k>
373-
374376 rule <k> #traverseProjection(DEST, SPLDataBuffer(VAL), .ProjectionElems, CTXTS) ~> #derefTruncate(dynamicSize (_), PROJS)
375377 => #traverseProjection(DEST, SPLDataBuffer(VAL), PROJS, CTXTS) ...
376378 </k>
0 commit comments