From fcb6be91b8818b00eee36f7eaab8c7d1e375f468 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Fri, 13 Mar 2026 14:19:37 -0500 Subject: [PATCH 1/8] Lemmas for inner_test_validate_owner (and expected_validate_owner_result helper) --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 4 + .../symbolic/inner_test_validate_owner.md | 1113 +++++++++++++++++ 2 files changed, 1117 insertions(+) create mode 100644 kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index f7c3fb480..b15d726c7 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -10,6 +10,7 @@ requires "intrinsics.md" requires "symbolic/p-token.md" requires "symbolic/spl-token.md" +requires "symbolic/inner_test_validate_owner.md" ``` ## Syntax of MIR in K @@ -719,5 +720,8 @@ module KMIR imports KMIR-P-TOKEN // cheat codes imports KMIR-SPL-TOKEN // SPL-specific cheat codes + imports VALIDATE-OWNER-COMMON + imports EXPECTED-VALIDATE-OWNER-RESULT-LEMMA + imports INNER-TEST-VALIDATE-OWNER-LEMMA endmodule ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md new file mode 100644 index 000000000..5057216dc --- /dev/null +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md @@ -0,0 +1,1113 @@ +```k +requires "../kmir-ast.md" +requires "../rt/data.md" +requires "../kmir.md" +requires "../rt/configuration.md" +requires "p-token.md" +``` + +## Common helpers for validate_owner lemmas + +Shared constants, projection helpers, and signer-checking functions used by +both `expected_validate_owner_result` and `inner_test_validate_owner` lemmas. + +```k +module VALIDATE-OWNER-COMMON + imports KMIR-P-TOKEN + + // Result<(), ProgramError> values used in rules below (inlined as Aggregates): + // Ok(()) = Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List))) + // Err(Custom(4)) = Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))) + // Err(MissingRequiredSignature) = Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) + // Err(UninitializedAccount) = Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(9), .List))) + // Err(InvalidAccountData) = Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(3), .List))) + + // SPL Token Program ID as a Key (32 bytes). + // Hex: 06 dd f6 e1 d7 65 a1 93 d9 cb e1 46 ce eb 79 ac + // 1c b4 85 ed 5f 5b 37 91 3a 8c f5 85 7e ff 00 a9 + syntax Key ::= "#programIdKey" [function, total] + rule #programIdKey => Key( + ListItem(Integer(6, 8, false)) ListItem(Integer(221, 8, false)) + ListItem(Integer(246, 8, false)) ListItem(Integer(225, 8, false)) + ListItem(Integer(215, 8, false)) ListItem(Integer(101, 8, false)) + ListItem(Integer(161, 8, false)) ListItem(Integer(147, 8, false)) + ListItem(Integer(217, 8, false)) ListItem(Integer(203, 8, false)) + ListItem(Integer(225, 8, false)) ListItem(Integer(70, 8, false)) + ListItem(Integer(206, 8, false)) ListItem(Integer(235, 8, false)) + ListItem(Integer(121, 8, false)) ListItem(Integer(172, 8, false)) + ListItem(Integer(28, 8, false)) ListItem(Integer(180, 8, false)) + ListItem(Integer(133, 8, false)) ListItem(Integer(237, 8, false)) + ListItem(Integer(95, 8, false)) ListItem(Integer(91, 8, false)) + ListItem(Integer(55, 8, false)) ListItem(Integer(145, 8, false)) + ListItem(Integer(58, 8, false)) ListItem(Integer(140, 8, false)) + ListItem(Integer(245, 8, false)) ListItem(Integer(133, 8, false)) + ListItem(Integer(126, 8, false)) ListItem(Integer(255, 8, false)) + ListItem(Integer(0, 8, false)) ListItem(Integer(169, 8, false)) + ) + + // Projection chain: from &[AccountInfo] Place to the ith tx_signer's + // Account Aggregate (9-field struct behind the AccountInfo pointer). + // Parameters: I = index, N = array length (min_length for ConstantIndex). + syntax ProjectionElems ::= #txSignerAccountProjs(Int, Int) [function, total] + rule #txSignerAccountProjs(I, N) => + projectionElemDeref + projectionElemConstantIndex(I, N, false) + projectionElemField(fieldIdx(0), #hack()) + projectionElemDeref + .ProjectionElems + + // ========================================================================= + // Common helpers for signer checking + // ========================================================================= + + syntax Int ::= #bool2Int(Bool) [function, total] + rule #bool2Int(true) => 1 + rule #bool2Int(false) => 0 + + // --- 3 tx_signers --- + syntax Bool ::= #unsignedExists3( Key, Key, Key, Value, Int, Value, Int, Value, Int ) [function, total] + rule #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + => ( IS0 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY0 orBool fromKey(SKEY1) ==K KEY0 orBool fromKey(SKEY2) ==K KEY0 ) ) + orBool ( IS1 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY1 orBool fromKey(SKEY1) ==K KEY1 orBool fromKey(SKEY2) ==K KEY1 ) ) + orBool ( IS2 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY2 orBool fromKey(SKEY1) ==K KEY2 orBool fromKey(SKEY2) ==K KEY2 ) ) + + syntax Bool ::= #signerMatched3( Key, Value, Int, Value, Int, Value, Int ) [function, total] + rule #signerMatched3(SK, KEY0, IS0, KEY1, IS1, KEY2, IS2) + => ( fromKey(SK) ==K KEY0 andBool IS0 =/=Int 0 ) + orBool ( fromKey(SK) ==K KEY1 andBool IS1 =/=Int 0 ) + orBool ( fromKey(SK) ==K KEY2 andBool IS2 =/=Int 0 ) + + syntax Int ::= #signersCount3( Key, Key, Key, Value, Int, Value, Int, Value, Int ) [function, total] + rule #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + => #bool2Int(#signerMatched3(SKEY0, KEY0, IS0, KEY1, IS1, KEY2, IS2)) + +Int #bool2Int(#signerMatched3(SKEY1, KEY0, IS0, KEY1, IS1, KEY2, IS2)) + +Int #bool2Int(#signerMatched3(SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2)) + + // --- 2 tx_signers --- + syntax Bool ::= #unsignedExists2( Key, Key, Key, Value, Int, Value, Int ) [function, total] + rule #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + => ( IS0 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY0 orBool fromKey(SKEY1) ==K KEY0 orBool fromKey(SKEY2) ==K KEY0 ) ) + orBool ( IS1 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY1 orBool fromKey(SKEY1) ==K KEY1 orBool fromKey(SKEY2) ==K KEY1 ) ) + + syntax Bool ::= #signerMatched2( Key, Value, Int, Value, Int ) [function, total] + rule #signerMatched2(SK, KEY0, IS0, KEY1, IS1) + => ( fromKey(SK) ==K KEY0 andBool IS0 =/=Int 0 ) + orBool ( fromKey(SK) ==K KEY1 andBool IS1 =/=Int 0 ) + + syntax Int ::= #signersCount2( Key, Key, Key, Value, Int, Value, Int ) [function, total] + rule #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + => #bool2Int(#signerMatched2(SKEY0, KEY0, IS0, KEY1, IS1)) + +Int #bool2Int(#signerMatched2(SKEY1, KEY0, IS0, KEY1, IS1)) + +Int #bool2Int(#signerMatched2(SKEY2, KEY0, IS0, KEY1, IS1)) + + // --- 1 tx_signer --- + syntax Bool ::= #unsignedExists1( Key, Key, Key, Value, Int ) [function, total] + rule #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + => IS0 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY0 orBool fromKey(SKEY1) ==K KEY0 orBool fromKey(SKEY2) ==K KEY0 ) + + syntax Bool ::= #signerMatched1( Key, Value, Int ) [function, total] + rule #signerMatched1(SK, KEY0, IS0) + => fromKey(SK) ==K KEY0 andBool IS0 =/=Int 0 + + syntax Int ::= #signersCount1( Key, Key, Key, Value, Int ) [function, total] + rule #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + => #bool2Int(#signerMatched1(SKEY0, KEY0, IS0)) + +Int #bool2Int(#signerMatched1(SKEY1, KEY0, IS0)) + +Int #bool2Int(#signerMatched1(SKEY2, KEY0, IS0)) + +endmodule +``` + +## Lemma rules for `expected_validate_owner_result` + +These intercept the call to `expected_validate_owner_result` and directly +produce the return value, bypassing the function body. + +```k +module EXPECTED-VALIDATE-OWNER-RESULT-LEMMA + imports VALIDATE-OWNER-COMMON + + // ========================================================================= + // Intercept rule and dispatch helper + // ========================================================================= + + syntax KItem ::= #validateOwnerResultExpected( Evaluation, Evaluation, Place, Evaluation, Place, MaybeBasicBlockIdx ) + [seqstrict(1,2,4)] + + rule [validate-owner-expected-intercept]: + #execTerminatorCall(_, FUNC, + operandCopy(place(LOCAL0, PROJS0)) + operandCopy(place(LOCAL1, PROJS1)) + operandCopy(place(LOCAL2, PROJS2)) + operandMove(PLACE3) + .Operands, + DEST, TARGET, _UNWIND, _SPAN) ~> _CONT + => #validateOwnerResultExpected( + operandCopy(place(LOCAL0, appendP(PROJS0, projectionElemDeref .ProjectionElems))), + operandCopy(place(LOCAL1, appendP(PROJS1, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems))), + place(LOCAL2, PROJS2), + operandCopy(PLACE3), + DEST, TARGET) + + requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::expected_validate_owner_result" + [priority(30)] + + // ========================================================================= + // Case 1: expected_owner != key!(owner_account_info) => Err(Custom(4)) + // ========================================================================= + rule [validate-owner-expected-wrong-owner-nonmultisig]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountAccount(PAcc(_,_,_,_,_, OWNER_KEY, _, _, _), _), + _, + _MAYBE_MULTISIG, + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false)))))) ~> #continueAt(TARGET) // Err(Custom(4)) + + requires EXPECTED_OWNER =/=K fromKey(OWNER_KEY) + [priority(30)] + + rule [validate-owner-expected-wrong-owner-multisig]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, _, _, _), _), + _, + _MAYBE_MULTISIG, + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false)))))) ~> #continueAt(TARGET) // Err(Custom(4)) + + requires EXPECTED_OWNER =/=K fromKey(OWNER_KEY) + [priority(30)] + + // ========================================================================= + // Case 2: non-multisig, not signer => Err(MissingRequiredSignature) + // ========================================================================= + rule [validate-owner-expected-nonmultisig-not-signer]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountAccount(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, _, _, _), _), + _, + Aggregate(variantIdx(0), .List), // None + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool IS_SIGNER ==Int 0 + [priority(30)] + + // ========================================================================= + // Case 3: non-multisig, is signer => Ok(()) + // ========================================================================= + rule [validate-owner-expected-nonmultisig-ok]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountAccount(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, _, _, _), _), + _, + Aggregate(variantIdx(0), .List), // None + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool IS_SIGNER =/=Int 0 + [priority(30)] + + // ========================================================================= + // Case 4: multisig fallthrough (owner!=PROGRAM_ID), not signer + // ========================================================================= + rule [validate-owner-expected-multisig-fallthrough-not-signer]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), _), // Some(...) + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT =/=K #programIdKey + andBool IS_SIGNER ==Int 0 + [priority(30)] + + // ========================================================================= + // Case 5: multisig fallthrough (owner!=PROGRAM_ID), is signer + // ========================================================================= + rule [validate-owner-expected-multisig-fallthrough-ok]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), _), // Some(...) + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT =/=K #programIdKey + andBool IS_SIGNER =/=Int 0 + [priority(30)] + + // ========================================================================= + // Case 6: multisig, is_initialized returns Err => Err(InvalidAccountData) + // ========================================================================= + rule [validate-owner-expected-multisig-invalid-data]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(3), .List))))), // Some(Err(InvalidAccountData)) + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(3), .List)))) ~> #continueAt(TARGET) // Err(InvalidAccountData) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + // ========================================================================= + // Case 7: multisig, is_initialized returns Ok(false) => Err(UninitializedAccount) + // ========================================================================= + rule [validate-owner-expected-multisig-uninitialized]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(false))))), // Some(Ok(false)) + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(9), .List)))) ~> #continueAt(TARGET) // Err(UninitializedAccount) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + // ========================================================================= + // Multisig signer-checking (Cases 8-10) + // ========================================================================= + + rule [validate-owner-expected-multisig-check-signers]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountMultisig( + PAcc(_, _, _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), + IMulti(U8(M), _, _, + Signers(ListItem(SKEY0) ListItem(SKEY1) ListItem(SKEY2)))), + place(LOCAL2, PROJS2), + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(true))))), // Some(Ok(true)) + DEST, TARGET) + => #resolveSignerCountExpected( + M, SKEY0, SKEY1, SKEY2, + operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), + place(LOCAL2, PROJS2), + DEST, TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + syntax KItem ::= #resolveSignerCountExpected( + Int, Key, Key, Key, + Evaluation, + Place, + Place, MaybeBasicBlockIdx + ) [seqstrict(5)] + + rule [resolve-3-signers-expected]: + #resolveSignerCountExpected( + M, SKEY0, SKEY1, SKEY2, + Range(ListItem(_) ListItem(_) ListItem(_)), + place(LOCAL2, PROJS2), + DEST, TARGET) + => #checkSigners3Expected( + M, SKEY0, SKEY1, SKEY2, + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 3)))), + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 3)))), + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(2, 3)))), + DEST, TARGET) + + [priority(30)] + + rule [resolve-2-signers-expected]: + #resolveSignerCountExpected( + M, SKEY0, SKEY1, SKEY2, + Range(ListItem(_) ListItem(_)), + place(LOCAL2, PROJS2), + DEST, TARGET) + => #checkSigners2Expected( + M, SKEY0, SKEY1, SKEY2, + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 2)))), + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 2)))), + DEST, TARGET) + + [priority(30)] + + rule [resolve-1-signer-expected]: + #resolveSignerCountExpected( + M, SKEY0, SKEY1, SKEY2, + Range(ListItem(_)), + place(LOCAL2, PROJS2), + DEST, TARGET) + => #checkSigners1Expected( + M, SKEY0, SKEY1, SKEY2, + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 1)))), + DEST, TARGET) + + [priority(30)] + + // --- 3 tx_signers --- + syntax KItem ::= #checkSigners3Expected( + Int, Key, Key, Key, + Evaluation, Evaluation, Evaluation, + Place, MaybeBasicBlockIdx + ) [seqstrict(5,6,7)] + + rule [validate-owner-expected-multisig-unsigned-3]: + #checkSigners3Expected( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + + requires #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + [priority(30)] + + rule [validate-owner-expected-multisig-not-enough-3]: + #checkSigners3Expected( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + + requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) #checkSigners3Expected( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) >=Int M + [priority(30)] + + // --- 2 tx_signers --- + syntax KItem ::= #checkSigners2Expected( + Int, Key, Key, Key, + Evaluation, Evaluation, + Place, MaybeBasicBlockIdx + ) [seqstrict(5,6)] + + rule [validate-owner-expected-multisig-unsigned-2]: + #checkSigners2Expected( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + + requires #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + [priority(30)] + + rule [validate-owner-expected-multisig-not-enough-2]: + #checkSigners2Expected( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + + requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) #checkSigners2Expected( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) >=Int M + [priority(30)] + + // --- 1 tx_signer --- + syntax KItem ::= #checkSigners1Expected( + Int, Key, Key, Key, + Evaluation, + Place, MaybeBasicBlockIdx + ) [seqstrict(5)] + + rule [validate-owner-expected-multisig-unsigned-1]: + #checkSigners1Expected( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + + requires #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + [priority(30)] + + rule [validate-owner-expected-multisig-not-enough-1]: + #checkSigners1Expected( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + + requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) #checkSigners1Expected( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) >=Int M + [priority(30)] + +endmodule +``` + +## Lemma rules for `inner_test_validate_owner` + +This function has the same branching logic as `expected_validate_owner_result`, +but takes an additional `result` parameter and asserts (`assert_eq!`) that it +matches the expected outcome at each error branch. The success path returns +`Ok(())` without asserting. + +```k +module INNER-TEST-VALIDATE-OWNER-LEMMA + imports VALIDATE-OWNER-COMMON + + // ========================================================================= + // Intercept rule and dispatch helper + // ========================================================================= + // + // inner_test_validate_owner has 5 arguments: + // ARG0: expected_owner (&Pubkey) - operandCopy + // ARG1: owner_account_info (&AccountInfo) - operandCopy + // ARG2: tx_signers (&[AccountInfo]) - operandCopy + // ARG3: maybe_multisig_is_initialised - operandMove + // ARG4: result (Result<(), ProgramError>) - operandMove + // + // Positions 1, 2, 4, 5 are Evaluation (evaluated by seqstrict). + // Position 3 is Place (tx_signers, unevaluated, used for projections). + syntax KItem ::= #validateOwnerResult( Evaluation, Evaluation, Place, Evaluation, Evaluation, Place, MaybeBasicBlockIdx ) + [seqstrict(1,2,4,5)] + // ^expected_owner + // ^owner_account (PAccount) + // ^tx_signers Place (NOT evaluated) + // ^maybe_multisig + // ^result + // ^DEST ^TARGET + + rule [inner-validate-owner-intercept]: + #execTerminatorCall(_, FUNC, + operandCopy(place(LOCAL0, PROJS0)) + operandCopy(place(LOCAL1, PROJS1)) + operandCopy(place(LOCAL2, PROJS2)) + operandMove(PLACE3) + operandMove(PLACE4) + .Operands, + DEST, TARGET, _UNWIND, _SPAN) ~> _CONT + => #validateOwnerResult( + // ARG0: deref &Pubkey to get Range(LIST) + operandCopy(place(LOCAL0, appendP(PROJS0, projectionElemDeref .ProjectionElems))), + // ARG1: deref &AccountInfo -> field(0) -> deref to get PAccount + operandCopy(place(LOCAL1, appendP(PROJS1, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) projectionElemDeref .ProjectionElems))), + // ARG2: pass Place through unevaluated (used by multisig phase 2) + place(LOCAL2, PROJS2), + // ARG3: evaluate the Option value + operandCopy(PLACE3), + // ARG4: evaluate the result value + operandCopy(PLACE4), + DEST, TARGET) + + requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::inner_test_validate_owner" + [priority(30)] + + // Custom MIRError for assert_eq failures in inner_test_validate_owner + syntax MIRError ::= "#ValidateOwnerAssertFailed" + + // ========================================================================= + // Case 1: expected_owner != key!(owner_account_info) => assert result == Err(Custom(4)) + // ========================================================================= + // Pass: result matches Err(Custom(4)) + rule [inner-validate-owner-wrong-owner-nonmultisig]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountAccount(PAcc(_,_,_,_,_, OWNER_KEY, _, _, _), _), + _, + _MAYBE_MULTISIG:Value, + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires EXPECTED_OWNER =/=K fromKey(OWNER_KEY) + [priority(30)] + + // Fail: result does not match Err(Custom(4)) + rule [inner-validate-owner-wrong-owner-nonmultisig-fail]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountAccount(PAcc(_,_,_,_,_, OWNER_KEY, _, _, _), _), + _, _MAYBE_MULTISIG:Value, RESULT:Value, _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires EXPECTED_OWNER =/=K fromKey(OWNER_KEY) + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))) + [priority(30)] + + // Pass: result matches Err(Custom(4)) + rule [inner-validate-owner-wrong-owner-multisig]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, _, _, _), _), + _, + _MAYBE_MULTISIG:Value, + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires EXPECTED_OWNER =/=K fromKey(OWNER_KEY) + [priority(30)] + + // Fail: result does not match Err(Custom(4)) + rule [inner-validate-owner-wrong-owner-multisig-fail]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, _, _, _), _), + _, _MAYBE_MULTISIG:Value, RESULT:Value, _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires EXPECTED_OWNER =/=K fromKey(OWNER_KEY) + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))) + [priority(30)] + + // ========================================================================= + // Case 2: non-multisig, not signer => assert result == Err(MissingRequiredSignature) + // ========================================================================= + // Pass: result matches Err(MissingRequiredSignature) + rule [inner-validate-owner-nonmultisig-not-signer]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountAccount(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, _, _, _), _), + _, + Aggregate(variantIdx(0), .List), // None + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool IS_SIGNER ==Int 0 + [priority(30)] + + // Fail: result does not match Err(MissingRequiredSignature) + rule [inner-validate-owner-nonmultisig-not-signer-fail]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountAccount(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, _, _, _), _), + _, + Aggregate(variantIdx(0), .List), // None + RESULT:Value, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool IS_SIGNER ==Int 0 + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) + [priority(30)] + + // ========================================================================= + // Case 3: non-multisig, is signer => Ok(()) (no assert on result) + // ========================================================================= + rule [inner-validate-owner-nonmultisig-ok]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountAccount(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, _, _, _), _), + _, + Aggregate(variantIdx(0), .List), // None + _RESULT, + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool IS_SIGNER =/=Int 0 + [priority(30)] + + // ========================================================================= + // Case 4: multisig fallthrough (owner!=PROGRAM_ID), not signer + // => assert result == Err(MissingRequiredSignature) + // ========================================================================= + // Pass: result matches Err(MissingRequiredSignature) + rule [inner-validate-owner-multisig-fallthrough-not-signer]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), _), // Some(...) + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT =/=K #programIdKey + andBool IS_SIGNER ==Int 0 + [priority(30)] + + // Fail: result does not match Err(MissingRequiredSignature) + rule [inner-validate-owner-multisig-fallthrough-not-signer-fail]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), _), // Some(...) + RESULT:Value, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT =/=K #programIdKey + andBool IS_SIGNER ==Int 0 + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) + [priority(30)] + + // ========================================================================= + // Case 5: multisig fallthrough (owner!=PROGRAM_ID), is signer => Ok(()) + // ========================================================================= + rule [inner-validate-owner-multisig-fallthrough-ok]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_, U8(IS_SIGNER), _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), _), // Some(...) + _RESULT, + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT =/=K #programIdKey + andBool IS_SIGNER =/=Int 0 + [priority(30)] + + // ========================================================================= + // Case 6: multisig, is_initialized returns Err + // => assert result == Err(InvalidAccountData) + // ========================================================================= + // Pass: result matches Err(InvalidAccountData) + rule [inner-validate-owner-multisig-invalid-data]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(3), .List))))), // Some(Err(InvalidAccountData)) + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(3), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + // Fail: result does not match Err(InvalidAccountData) + rule [inner-validate-owner-multisig-invalid-data-fail]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(3), .List))))), // Some(Err(InvalidAccountData)) + RESULT:Value, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(3), .List))) + [priority(30)] + + // ========================================================================= + // Case 7: multisig, is_initialized returns Ok(false) + // => assert result == Err(UninitializedAccount) + // ========================================================================= + // Pass: result matches Err(UninitializedAccount) + rule [inner-validate-owner-multisig-uninitialized]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(false))))), // Some(Ok(false)) + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(9), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + // Fail: result does not match Err(UninitializedAccount) + rule [inner-validate-owner-multisig-uninitialized-fail]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), _), + _, + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(false))))), // Some(Ok(false)) + RESULT:Value, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(9), .List))) + [priority(30)] + + // ========================================================================= + // Multisig signer-checking (Cases 8-10) + // ========================================================================= + + rule [inner-validate-owner-multisig-check-signers]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig( + PAcc(_, _, _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), + IMulti(U8(M), _, _, + Signers(ListItem(SKEY0) ListItem(SKEY1) ListItem(SKEY2)))), + place(LOCAL2, PROJS2), + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(true))))), // Some(Ok(true)) + RESULT, + DEST, TARGET) + => #resolveSignerCount( + M, SKEY0, SKEY1, SKEY2, + operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), + place(LOCAL2, PROJS2), + RESULT, + DEST, TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + syntax KItem ::= #resolveSignerCount( + Int, Key, Key, Key, + Evaluation, // 5: deref'd slice (evaluates to array value) + Place, // 6: original tx_signers Place + Value, // 7: RESULT + Place, MaybeBasicBlockIdx + ) [seqstrict(5)] + + // Dispatch: 3 tx_signers + rule [resolve-3-signers]: + #resolveSignerCount( + M, SKEY0, SKEY1, SKEY2, + Range(ListItem(_) ListItem(_) ListItem(_)), + place(LOCAL2, PROJS2), + RESULT, + DEST, TARGET) + => #checkSigners3( + M, SKEY0, SKEY1, SKEY2, + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 3)))), + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 3)))), + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(2, 3)))), + RESULT, + DEST, TARGET) + + [priority(30)] + + // Dispatch: 2 tx_signers + rule [resolve-2-signers]: + #resolveSignerCount( + M, SKEY0, SKEY1, SKEY2, + Range(ListItem(_) ListItem(_)), + place(LOCAL2, PROJS2), + RESULT, + DEST, TARGET) + => #checkSigners2( + M, SKEY0, SKEY1, SKEY2, + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 2)))), + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 2)))), + RESULT, + DEST, TARGET) + + [priority(30)] + + // Dispatch: 1 tx_signer + rule [resolve-1-signer]: + #resolveSignerCount( + M, SKEY0, SKEY1, SKEY2, + Range(ListItem(_)), + place(LOCAL2, PROJS2), + RESULT, + DEST, TARGET) + => #checkSigners1( + M, SKEY0, SKEY1, SKEY2, + operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 1)))), + RESULT, + DEST, TARGET) + + [priority(30)] + + // ========================================================================= + // 3 tx_signers: #checkSigners3 + // ========================================================================= + + syntax KItem ::= #checkSigners3( + Int, Key, Key, Key, + Evaluation, Evaluation, Evaluation, + Value, // 8: RESULT + Place, MaybeBasicBlockIdx + ) [seqstrict(5,6,7)] + + // Case 8a: unsigned signer exists => assert result == Err(MissingRequiredSignature) + rule [inner-validate-owner-multisig-unsigned-3]: + #checkSigners3( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + [priority(30)] + + rule [inner-validate-owner-multisig-unsigned-3-fail]: + #checkSigners3( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + RESULT, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) + [priority(30)] + + // Case 9a: not enough signers => assert result == Err(MissingRequiredSignature) + rule [inner-validate-owner-multisig-not-enough-3]: + #checkSigners3( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) #checkSigners3( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + RESULT, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) Ok(()) (no assert on result) + rule [inner-validate-owner-multisig-ok-3]: + #checkSigners3( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + _RESULT, + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) >=Int M + [priority(30)] + + // ========================================================================= + // 2 tx_signers: #checkSigners2 + // ========================================================================= + + syntax KItem ::= #checkSigners2( + Int, Key, Key, Key, + Evaluation, Evaluation, + Value, // 7: RESULT + Place, MaybeBasicBlockIdx + ) [seqstrict(5,6)] + + // Case 8b: unsigned signer exists (2 tx_signers) + rule [inner-validate-owner-multisig-unsigned-2]: + #checkSigners2( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + [priority(30)] + + rule [inner-validate-owner-multisig-unsigned-2-fail]: + #checkSigners2( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + RESULT, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) + [priority(30)] + + // Case 9b: not enough signers (2 tx_signers) + rule [inner-validate-owner-multisig-not-enough-2]: + #checkSigners2( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) #checkSigners2( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + RESULT, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) Ok(()) + rule [inner-validate-owner-multisig-ok-2]: + #checkSigners2( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + _RESULT, + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) >=Int M + [priority(30)] + + // ========================================================================= + // 1 tx_signer: #checkSigners1 + // ========================================================================= + + syntax KItem ::= #checkSigners1( + Int, Key, Key, Key, + Evaluation, + Value, // 6: RESULT + Place, MaybeBasicBlockIdx + ) [seqstrict(5)] + + // Case 8c: unsigned signer exists (1 tx_signer) + rule [inner-validate-owner-multisig-unsigned-1]: + #checkSigners1( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + [priority(30)] + + rule [inner-validate-owner-multisig-unsigned-1-fail]: + #checkSigners1( + _M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + RESULT, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) + [priority(30)] + + // Case 9c: not enough signers (1 tx_signer) + rule [inner-validate-owner-multisig-not-enough-1]: + #checkSigners1( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, + DEST, TARGET) + => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) + + requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) #checkSigners1( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + RESULT, + _DEST, _TARGET) + => #ValidateOwnerAssertFailed + + requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) Ok(()) + rule [inner-validate-owner-multisig-ok-1]: + #checkSigners1( + M, SKEY0, SKEY1, SKEY2, + Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), + _RESULT, + DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + + requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) >=Int M + [priority(30)] + +endmodule +``` From 57e8638a533618c63880ae1d101fc97386f86fc6 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Fri, 13 Mar 2026 15:29:58 -0500 Subject: [PATCH 2/8] Removed unneeded import. --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 1 - 1 file changed, 1 deletion(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index b15d726c7..cd8e255a7 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -720,7 +720,6 @@ module KMIR imports KMIR-P-TOKEN // cheat codes imports KMIR-SPL-TOKEN // SPL-specific cheat codes - imports VALIDATE-OWNER-COMMON imports EXPECTED-VALIDATE-OWNER-RESULT-LEMMA imports INNER-TEST-VALIDATE-OWNER-LEMMA endmodule From 7fa3b003c8459aff46dbf3111c3ba832bed15234 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Fri, 13 Mar 2026 16:04:05 -0500 Subject: [PATCH 3/8] Renamed modules. --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 4 ++-- .../kdist/mir-semantics/symbolic/inner_test_validate_owner.md | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index cd8e255a7..a3bd623fe 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -720,7 +720,7 @@ module KMIR imports KMIR-P-TOKEN // cheat codes imports KMIR-SPL-TOKEN // SPL-specific cheat codes - imports EXPECTED-VALIDATE-OWNER-RESULT-LEMMA - imports INNER-TEST-VALIDATE-OWNER-LEMMA + imports EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA + imports INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA endmodule ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md index 5057216dc..3b7970b82 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md @@ -124,7 +124,7 @@ These intercept the call to `expected_validate_owner_result` and directly produce the return value, bypassing the function body. ```k -module EXPECTED-VALIDATE-OWNER-RESULT-LEMMA +module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA imports VALIDATE-OWNER-COMMON // ========================================================================= @@ -493,7 +493,7 @@ matches the expected outcome at each error branch. The success path returns `Ok(())` without asserting. ```k -module INNER-TEST-VALIDATE-OWNER-LEMMA +module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA imports VALIDATE-OWNER-COMMON // ========================================================================= From 77d808356b1da704f9bb858c3e6f90206253c5aa Mon Sep 17 00:00:00 2001 From: mariaKt Date: Fri, 13 Mar 2026 22:57:49 -0500 Subject: [PATCH 4/8] Improved error messages. --- .../symbolic/inner_test_validate_owner.md | 40 +++++++++++++------ 1 file changed, 27 insertions(+), 13 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md index 3b7970b82..eb9c947bc 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md @@ -22,6 +22,20 @@ module VALIDATE-OWNER-COMMON // Err(UninitializedAccount) = Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(9), .List))) // Err(InvalidAccountData) = Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(3), .List))) + // Convert a Result<(), ProgramError> Value to a human-readable string + syntax String ::= Result2String ( Value ) [function, total] + rule Result2String(Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) + => "Ok(())" + rule Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false)))))) + => "Err(Custom(4))" + rule Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) + => "Err(MissingRequiredSignature)" + rule Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(9), .List)))) + => "Err(UninitializedAccount)" + rule Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(3), .List)))) + => "Err(InvalidAccountData)" + rule Result2String(_) => "Unknown" [owise] + // SPL Token Program ID as a Key (32 bytes). // Hex: 06 dd f6 e1 d7 65 a1 93 d9 cb e1 46 ce eb 79 ac // 1c b4 85 ed 5f 5b 37 91 3a 8c f5 85 7e ff 00 a9 @@ -544,7 +558,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA [priority(30)] // Custom MIRError for assert_eq failures in inner_test_validate_owner - syntax MIRError ::= "#ValidateOwnerAssertFailed" + syntax MIRError ::= "#ValidateOwnerAssertFailed" "(" String ")" // ========================================================================= // Case 1: expected_owner != key!(owner_account_info) => assert result == Err(Custom(4)) @@ -569,7 +583,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA EXPECTED_OWNER, PAccountAccount(PAcc(_,_,_,_,_, OWNER_KEY, _, _, _), _), _, _MAYBE_MULTISIG:Value, RESULT:Value, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))))) requires EXPECTED_OWNER =/=K fromKey(OWNER_KEY) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))) @@ -595,7 +609,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA EXPECTED_OWNER, PAccountMultisig(PAcc(_,_,_,_,_, OWNER_KEY, _, _, _), _), _, _MAYBE_MULTISIG:Value, RESULT:Value, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))))) requires EXPECTED_OWNER =/=K fromKey(OWNER_KEY) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(0), ListItem(Integer(4, 32, false))))) @@ -628,7 +642,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA Aggregate(variantIdx(0), .List), // None RESULT:Value, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) andBool IS_SIGNER ==Int 0 @@ -681,7 +695,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA Aggregate(variantIdx(1), _), // Some(...) RESULT:Value, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) andBool OWNER_OF_ACCOUNT =/=K #programIdKey @@ -739,7 +753,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA Aggregate(variantIdx(3), .List))))), // Some(Err(InvalidAccountData)) RESULT:Value, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(3), .List))))) requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) andBool OWNER_OF_ACCOUNT ==K #programIdKey @@ -778,7 +792,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA BoolVal(false))))), // Some(Ok(false)) RESULT:Value, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(9), .List))))) requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) andBool OWNER_OF_ACCOUNT ==K #programIdKey @@ -905,7 +919,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), RESULT, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) requires #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) @@ -934,7 +948,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), RESULT, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) requires #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) @@ -1014,7 +1028,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), RESULT, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) requires #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) @@ -1089,7 +1103,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), RESULT, _DEST, _TARGET) - => #ValidateOwnerAssertFailed + => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) Date: Mon, 23 Mar 2026 11:47:57 -0500 Subject: [PATCH 5/8] Updated lemmas for new version of semantics and tests. --- .../symbolic/inner_test_validate_owner.md | 552 ++++++++++++------ 1 file changed, 362 insertions(+), 190 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md index eb9c947bc..954daec09 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md @@ -78,56 +78,63 @@ module VALIDATE-OWNER-COMMON rule #bool2Int(true) => 1 rule #bool2Int(false) => 0 - // --- 3 tx_signers --- - syntax Bool ::= #unsignedExists3( Key, Key, Key, Value, Int, Value, Int, Value, Int ) [function, total] - rule #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) - => ( IS0 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY0 orBool fromKey(SKEY1) ==K KEY0 orBool fromKey(SKEY2) ==K KEY0 ) ) - orBool ( IS1 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY1 orBool fromKey(SKEY1) ==K KEY1 orBool fromKey(SKEY2) ==K KEY1 ) ) - orBool ( IS2 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY2 orBool fromKey(SKEY1) ==K KEY2 orBool fromKey(SKEY2) ==K KEY2 ) ) - - syntax Bool ::= #signerMatched3( Key, Value, Int, Value, Int, Value, Int ) [function, total] - rule #signerMatched3(SK, KEY0, IS0, KEY1, IS1, KEY2, IS2) - => ( fromKey(SK) ==K KEY0 andBool IS0 =/=Int 0 ) - orBool ( fromKey(SK) ==K KEY1 andBool IS1 =/=Int 0 ) - orBool ( fromKey(SK) ==K KEY2 andBool IS2 =/=Int 0 ) - - syntax Int ::= #signersCount3( Key, Key, Key, Value, Int, Value, Int, Value, Int ) [function, total] - rule #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) - => #bool2Int(#signerMatched3(SKEY0, KEY0, IS0, KEY1, IS1, KEY2, IS2)) - +Int #bool2Int(#signerMatched3(SKEY1, KEY0, IS0, KEY1, IS1, KEY2, IS2)) - +Int #bool2Int(#signerMatched3(SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2)) - - // --- 2 tx_signers --- - syntax Bool ::= #unsignedExists2( Key, Key, Key, Value, Int, Value, Int ) [function, total] - rule #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) - => ( IS0 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY0 orBool fromKey(SKEY1) ==K KEY0 orBool fromKey(SKEY2) ==K KEY0 ) ) - orBool ( IS1 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY1 orBool fromKey(SKEY1) ==K KEY1 orBool fromKey(SKEY2) ==K KEY1 ) ) - - syntax Bool ::= #signerMatched2( Key, Value, Int, Value, Int ) [function, total] - rule #signerMatched2(SK, KEY0, IS0, KEY1, IS1) - => ( fromKey(SK) ==K KEY0 andBool IS0 =/=Int 0 ) - orBool ( fromKey(SK) ==K KEY1 andBool IS1 =/=Int 0 ) - - syntax Int ::= #signersCount2( Key, Key, Key, Value, Int, Value, Int ) [function, total] - rule #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) - => #bool2Int(#signerMatched2(SKEY0, KEY0, IS0, KEY1, IS1)) - +Int #bool2Int(#signerMatched2(SKEY1, KEY0, IS0, KEY1, IS1)) - +Int #bool2Int(#signerMatched2(SKEY2, KEY0, IS0, KEY1, IS1)) - - // --- 1 tx_signer --- - syntax Bool ::= #unsignedExists1( Key, Key, Key, Value, Int ) [function, total] - rule #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) - => IS0 ==Int 0 andBool ( fromKey(SKEY0) ==K KEY0 orBool fromKey(SKEY1) ==K KEY0 orBool fromKey(SKEY2) ==K KEY0 ) - - syntax Bool ::= #signerMatched1( Key, Value, Int ) [function, total] - rule #signerMatched1(SK, KEY0, IS0) - => fromKey(SK) ==K KEY0 andBool IS0 =/=Int 0 + // ========================================================================= + // Generic signer checking helpers (list-based) + // + // These work for any number of tx_signers and registered signers. + // The caller constructs lists from the extracted values. + // + // keyAndIsSigner(KEY, IS) pairs a tx_signer's public key with its is_signer flag. + // firstN(N, LIST) takes the first N elements of LIST (implements [0..n] slicing). + // + // #unsignedExists(TxSigners, RegisteredKeys): + // outer loop over tx_signers, inner loop over registered keys. + // True if any tx_signer matches a registered key and is NOT a signer. + // + // #signersCount(TxSigners, RegisteredKeys): + // outer loop over registered keys, inner loop over tx_signers. + // Counts how many registered keys have a matching signed tx_signer. + // ========================================================================= - syntax Int ::= #signersCount1( Key, Key, Key, Value, Int ) [function, total] - rule #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) - => #bool2Int(#signerMatched1(SKEY0, KEY0, IS0)) - +Int #bool2Int(#signerMatched1(SKEY1, KEY0, IS0)) - +Int #bool2Int(#signerMatched1(SKEY2, KEY0, IS0)) + syntax KeyAndIsSigner ::= keyAndIsSigner( Value, Int ) + + syntax List ::= firstN( Int, List ) [function, total] + // ------------------------------------------------- + rule firstN(0, _) => .List + rule firstN(N, ListItem(X) REST) => ListItem(X) firstN(N -Int 1, REST) requires N >Int 0 + rule firstN(_, .List) => .List [owise] + + // --- #unsignedExists: outer over tx_signers, inner over registered keys --- + + syntax Bool ::= #unsignedExists( List, List ) [function] + // ----------------------------------------------------------- + rule #unsignedExists(.List, _REGS) => false + rule #unsignedExists(ListItem(keyAndIsSigner(KEY, IS)) REST, REGS) + => #unsignedExistsInner(KEY, IS, REGS) + orBool #unsignedExists(REST, REGS) + + syntax Bool ::= #unsignedExistsInner( Value, Int, List ) [function] + // ----------------------------------------------------------------------- + rule #unsignedExistsInner(_KEY, _IS, .List) => false + rule #unsignedExistsInner(KEY, IS, ListItem(SKEY) REST) + => ( IS ==Int 0 andBool fromKey(SKEY) ==K KEY ) + orBool #unsignedExistsInner(KEY, IS, REST) + + // --- #signersCount: outer over registered keys, inner over tx_signers --- + + syntax Int ::= #signersCount( List, List ) [function] + // --------------------------------------------------------- + rule #signersCount(_TXSIGNERS, .List) => 0 + rule #signersCount(TXSIGNERS, ListItem(SKEY) REST) + => #bool2Int(#signerMatchedInner(SKEY, TXSIGNERS)) + +Int #signersCount(TXSIGNERS, REST) + + syntax Bool ::= #signerMatchedInner( Key, List ) [function] + // --------------------------------------------------------------- + rule #signerMatchedInner(_SKEY, .List) => false + rule #signerMatchedInner(SKEY, ListItem(keyAndIsSigner(KEY, IS)) REST) + => ( fromKey(SKEY) ==K KEY andBool IS =/=Int 0 ) + orBool #signerMatchedInner(SKEY, REST) endmodule ``` @@ -299,20 +306,67 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA // Multisig signer-checking (Cases 8-10) // ========================================================================= - rule [validate-owner-expected-multisig-check-signers]: + // N=3: all registered signers + rule [validate-owner-expected-multisig-check-signers-n3]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountMultisig( + PAcc(_, _, _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), + IMulti(U8(M), U8(3), _, // N=3 + Signers(SKEYS))), + place(LOCAL2, PROJS2), + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(true))))), // Some(Ok(true)) + DEST, TARGET) + => #resolveSignerCountExpected( + M, SKEYS, + operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), + place(LOCAL2, PROJS2), + DEST, TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + // N=2: first 2 registered signers + rule [validate-owner-expected-multisig-check-signers-n2]: #validateOwnerResultExpected( EXPECTED_OWNER, PAccountMultisig( PAcc(_, _, _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), - IMulti(U8(M), _, _, - Signers(ListItem(SKEY0) ListItem(SKEY1) ListItem(SKEY2)))), + IMulti(U8(M), U8(2), _, // N=2 + Signers(SKEYS))), place(LOCAL2, PROJS2), Aggregate(variantIdx(1), ListItem( Aggregate(variantIdx(0), ListItem( BoolVal(true))))), // Some(Ok(true)) DEST, TARGET) => #resolveSignerCountExpected( - M, SKEY0, SKEY1, SKEY2, + M, firstN(2, SKEYS), + operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), + place(LOCAL2, PROJS2), + DEST, TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + // N=1: first registered signer only + rule [validate-owner-expected-multisig-check-signers-n1]: + #validateOwnerResultExpected( + EXPECTED_OWNER, + PAccountMultisig( + PAcc(_, _, _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), + IMulti(U8(M), U8(1), _, // N=1 + Signers(SKEYS))), + place(LOCAL2, PROJS2), + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(true))))), // Some(Ok(true)) + DEST, TARGET) + => #resolveSignerCountExpected( + M, firstN(1, SKEYS), operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), place(LOCAL2, PROJS2), DEST, TARGET) @@ -322,20 +376,20 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA [priority(30)] syntax KItem ::= #resolveSignerCountExpected( - Int, Key, Key, Key, + Int, List, // M, REGS (already-sliced registered keys) Evaluation, Place, Place, MaybeBasicBlockIdx - ) [seqstrict(5)] + ) [seqstrict(3)] rule [resolve-3-signers-expected]: #resolveSignerCountExpected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Range(ListItem(_) ListItem(_) ListItem(_)), place(LOCAL2, PROJS2), DEST, TARGET) => #checkSigners3Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 3)))), operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 3)))), operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(2, 3)))), @@ -345,12 +399,12 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA rule [resolve-2-signers-expected]: #resolveSignerCountExpected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Range(ListItem(_) ListItem(_)), place(LOCAL2, PROJS2), DEST, TARGET) => #checkSigners2Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 2)))), operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 2)))), DEST, TARGET) @@ -359,141 +413,175 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA rule [resolve-1-signer-expected]: #resolveSignerCountExpected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Range(ListItem(_)), place(LOCAL2, PROJS2), DEST, TARGET) => #checkSigners1Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 1)))), DEST, TARGET) [priority(30)] // --- 3 tx_signers --- + // After evaluating the 3 tx_signer accounts, use generic list-based helpers. + syntax KItem ::= #checkSigners3Expected( - Int, Key, Key, Key, + Int, List, // M, REGS Evaluation, Evaluation, Evaluation, Place, MaybeBasicBlockIdx - ) [seqstrict(5,6,7)] + ) [seqstrict(3,4,5)] rule [validate-owner-expected-multisig-unsigned-3]: #checkSigners3Expected( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) - requires #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), + REGS) [priority(30)] rule [validate-owner-expected-multisig-not-enough-3]: #checkSigners3Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) - requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) - andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) #checkSigners3Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) - requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) - andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) >=Int M + requires notBool #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), + REGS) + andBool #signersCount( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), + REGS) >=Int M [priority(30)] // --- 2 tx_signers --- + syntax KItem ::= #checkSigners2Expected( - Int, Key, Key, Key, + Int, List, // M, REGS Evaluation, Evaluation, Place, MaybeBasicBlockIdx - ) [seqstrict(5,6)] + ) [seqstrict(3,4)] rule [validate-owner-expected-multisig-unsigned-2]: #checkSigners2Expected( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) - requires #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), + REGS) [priority(30)] rule [validate-owner-expected-multisig-not-enough-2]: #checkSigners2Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) - requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) - andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) #checkSigners2Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) - requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) - andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) >=Int M + requires notBool #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), + REGS) + andBool #signersCount( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), + REGS) >=Int M [priority(30)] // --- 1 tx_signer --- + syntax KItem ::= #checkSigners1Expected( - Int, Key, Key, Key, + Int, List, // M, REGS Evaluation, Place, MaybeBasicBlockIdx - ) [seqstrict(5)] + ) [seqstrict(3)] rule [validate-owner-expected-multisig-unsigned-1]: #checkSigners1Expected( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) - requires #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)), + REGS) [priority(30)] rule [validate-owner-expected-multisig-not-enough-1]: #checkSigners1Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) - requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) - andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) #checkSigners1Expected( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) - requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) - andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) >=Int M + requires notBool #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)), + REGS) + andBool #signersCount( + ListItem(keyAndIsSigner(KEY0, IS0)), + REGS) >=Int M [priority(30)] endmodule @@ -801,15 +889,42 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA // ========================================================================= // Multisig signer-checking (Cases 8-10) + // Uses generic list-based #unsignedExists and #signersCount helpers. // ========================================================================= - rule [inner-validate-owner-multisig-check-signers]: + // N=3: all registered signers + rule [inner-validate-owner-multisig-check-signers-n3]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig( + PAcc(_, _, _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), + IMulti(U8(M), U8(3), _, // N=3 + Signers(SKEYS))), + place(LOCAL2, PROJS2), + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(true))))), // Some(Ok(true)) + RESULT, + DEST, TARGET) + => #resolveSignerCount( + M, SKEYS, + operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), + place(LOCAL2, PROJS2), + RESULT, + DEST, TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + // N=2: first 2 registered signers + rule [inner-validate-owner-multisig-check-signers-n2]: #validateOwnerResult( EXPECTED_OWNER, PAccountMultisig( PAcc(_, _, _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), - IMulti(U8(M), _, _, - Signers(ListItem(SKEY0) ListItem(SKEY1) ListItem(SKEY2)))), + IMulti(U8(M), U8(2), _, // N=2 + Signers(SKEYS))), place(LOCAL2, PROJS2), Aggregate(variantIdx(1), ListItem( Aggregate(variantIdx(0), ListItem( @@ -817,7 +932,32 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA RESULT, DEST, TARGET) => #resolveSignerCount( - M, SKEY0, SKEY1, SKEY2, + M, firstN(2, SKEYS), + operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), + place(LOCAL2, PROJS2), + RESULT, + DEST, TARGET) + + requires EXPECTED_OWNER ==K fromKey(OWNER_KEY) + andBool OWNER_OF_ACCOUNT ==K #programIdKey + [priority(30)] + + // N=1: first registered signer only + rule [inner-validate-owner-multisig-check-signers-n1]: + #validateOwnerResult( + EXPECTED_OWNER, + PAccountMultisig( + PAcc(_, _, _,_,_, OWNER_KEY, OWNER_OF_ACCOUNT, _, _), + IMulti(U8(M), U8(1), _, // N=1 + Signers(SKEYS))), + place(LOCAL2, PROJS2), + Aggregate(variantIdx(1), ListItem( + Aggregate(variantIdx(0), ListItem( + BoolVal(true))))), // Some(Ok(true)) + RESULT, + DEST, TARGET) + => #resolveSignerCount( + M, firstN(1, SKEYS), operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), place(LOCAL2, PROJS2), RESULT, @@ -828,23 +968,23 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA [priority(30)] syntax KItem ::= #resolveSignerCount( - Int, Key, Key, Key, - Evaluation, // 5: deref'd slice (evaluates to array value) - Place, // 6: original tx_signers Place - Value, // 7: RESULT + Int, List, // M, REGS (already-sliced registered keys) + Evaluation, // 3: deref'd slice (evaluates to array value) + Place, // 4: original tx_signers Place + Value, // 5: RESULT Place, MaybeBasicBlockIdx - ) [seqstrict(5)] + ) [seqstrict(3)] // Dispatch: 3 tx_signers rule [resolve-3-signers]: #resolveSignerCount( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Range(ListItem(_) ListItem(_) ListItem(_)), place(LOCAL2, PROJS2), RESULT, DEST, TARGET) => #checkSigners3( - M, SKEY0, SKEY1, SKEY2, + M, REGS, operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 3)))), operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 3)))), operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(2, 3)))), @@ -856,13 +996,13 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA // Dispatch: 2 tx_signers rule [resolve-2-signers]: #resolveSignerCount( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Range(ListItem(_) ListItem(_)), place(LOCAL2, PROJS2), RESULT, DEST, TARGET) => #checkSigners2( - M, SKEY0, SKEY1, SKEY2, + M, REGS, operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 2)))), operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 2)))), RESULT, @@ -873,13 +1013,13 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA // Dispatch: 1 tx_signer rule [resolve-1-signer]: #resolveSignerCount( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Range(ListItem(_)), place(LOCAL2, PROJS2), RESULT, DEST, TARGET) => #checkSigners1( - M, SKEY0, SKEY1, SKEY2, + M, REGS, operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 1)))), RESULT, DEST, TARGET) @@ -888,19 +1028,20 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA // ========================================================================= // 3 tx_signers: #checkSigners3 + // Uses generic list-based #unsignedExists and #signersCount helpers. // ========================================================================= syntax KItem ::= #checkSigners3( - Int, Key, Key, Key, + Int, List, // M, REGS Evaluation, Evaluation, Evaluation, - Value, // 8: RESULT + Value, // 6: RESULT Place, MaybeBasicBlockIdx - ) [seqstrict(5,6,7)] + ) [seqstrict(3,4,5)] - // Case 8a: unsigned signer exists => assert result == Err(MissingRequiredSignature) + // Case 8: unsigned signer exists => assert result == Err(MissingRequiredSignature) rule [inner-validate-owner-multisig-unsigned-3]: #checkSigners3( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), @@ -908,12 +1049,14 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA DEST, TARGET) => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - requires #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), + REGS) [priority(30)] rule [inner-validate-owner-multisig-unsigned-3-fail]: #checkSigners3( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), @@ -921,14 +1064,16 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA _DEST, _TARGET) => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - requires #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), + REGS) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) [priority(30)] - // Case 9a: not enough signers => assert result == Err(MissingRequiredSignature) + // Case 9: not enough signers => assert result == Err(MissingRequiredSignature) rule [inner-validate-owner-multisig-not-enough-3]: #checkSigners3( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), @@ -936,13 +1081,17 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA DEST, TARGET) => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) - andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) #checkSigners3( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), @@ -950,15 +1099,19 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA _DEST, _TARGET) => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) - andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) Ok(()) (no assert on result) + // Case 10: enough signers => Ok(()) (no assert on result) rule [inner-validate-owner-multisig-ok-3]: #checkSigners3( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), @@ -966,162 +1119,181 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA DEST, TARGET) => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) - requires notBool #unsignedExists3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) - andBool #signersCount3(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1, KEY2, IS2) >=Int M + requires notBool #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), + REGS) + andBool #signersCount( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), + REGS) >=Int M [priority(30)] - // ========================================================================= - // 2 tx_signers: #checkSigners2 - // ========================================================================= + // --- 2 tx_signers --- syntax KItem ::= #checkSigners2( - Int, Key, Key, Key, + Int, List, // M, REGS Evaluation, Evaluation, - Value, // 7: RESULT + Value, // 5: RESULT Place, MaybeBasicBlockIdx - ) [seqstrict(5,6)] + ) [seqstrict(3,4)] - // Case 8b: unsigned signer exists (2 tx_signers) rule [inner-validate-owner-multisig-unsigned-2]: #checkSigners2( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, DEST, TARGET) => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - requires #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), + REGS) [priority(30)] rule [inner-validate-owner-multisig-unsigned-2-fail]: #checkSigners2( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - RESULT, - _DEST, _TARGET) + RESULT, _DEST, _TARGET) => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - requires #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), + REGS) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) [priority(30)] - // Case 9b: not enough signers (2 tx_signers) rule [inner-validate-owner-multisig-not-enough-2]: #checkSigners2( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, DEST, TARGET) => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) - andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) #checkSigners2( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - RESULT, - _DEST, _TARGET) + RESULT, _DEST, _TARGET) => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) - andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) Ok(()) rule [inner-validate-owner-multisig-ok-2]: #checkSigners2( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - _RESULT, - DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + _RESULT, DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) - requires notBool #unsignedExists2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) - andBool #signersCount2(SKEY0, SKEY1, SKEY2, KEY0, IS0, KEY1, IS1) >=Int M + requires notBool #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), + REGS) + andBool #signersCount( + ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), + REGS) >=Int M [priority(30)] - // ========================================================================= - // 1 tx_signer: #checkSigners1 - // ========================================================================= + // --- 1 tx_signer --- syntax KItem ::= #checkSigners1( - Int, Key, Key, Key, + Int, List, // M, REGS Evaluation, - Value, // 6: RESULT + Value, // 4: RESULT Place, MaybeBasicBlockIdx - ) [seqstrict(5)] + ) [seqstrict(3)] - // Case 8c: unsigned signer exists (1 tx_signer) rule [inner-validate-owner-multisig-unsigned-1]: #checkSigners1( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, DEST, TARGET) => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - requires #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)), + REGS) [priority(30)] rule [inner-validate-owner-multisig-unsigned-1-fail]: #checkSigners1( - _M, SKEY0, SKEY1, SKEY2, + _M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - RESULT, - _DEST, _TARGET) + RESULT, _DEST, _TARGET) => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - requires #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) + requires #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)), + REGS) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) [priority(30)] - // Case 9c: not enough signers (1 tx_signer) rule [inner-validate-owner-multisig-not-enough-1]: #checkSigners1( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, DEST, TARGET) => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) - andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) #checkSigners1( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - RESULT, - _DEST, _TARGET) + RESULT, _DEST, _TARGET) => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) - andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) Ok(()) rule [inner-validate-owner-multisig-ok-1]: #checkSigners1( - M, SKEY0, SKEY1, SKEY2, + M, REGS, Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - _RESULT, - DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) + _RESULT, DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) - requires notBool #unsignedExists1(SKEY0, SKEY1, SKEY2, KEY0, IS0) - andBool #signersCount1(SKEY0, SKEY1, SKEY2, KEY0, IS0) >=Int M + requires notBool #unsignedExists( + ListItem(keyAndIsSigner(KEY0, IS0)), + REGS) + andBool #signersCount( + ListItem(keyAndIsSigner(KEY0, IS0)), + REGS) >=Int M [priority(30)] endmodule -``` From 49837924a8b437cadd7255b6222030eec1871b83 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Mon, 23 Mar 2026 19:36:56 -0500 Subject: [PATCH 6/8] Removed hard-coded tx signers list and rules, rules to heat-cool List instead. --- .../symbolic/inner_test_validate_owner.md | 619 ++++++------------ 1 file changed, 203 insertions(+), 416 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md index 954daec09..6b064cd86 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md @@ -136,6 +136,23 @@ module VALIDATE-OWNER-COMMON => ( fromKey(SKEY) ==K KEY andBool IS =/=Int 0 ) orBool #signerMatchedInner(SKEY, REST) + // ========================================================================= + // Extract key and is_signer from a list of evaluated tx_signer account + // Values. Each account is an Aggregate with 9 fields; field 1 (0-indexed) + // is is_signer (u8), field 5 is the account key (Range of 32 bytes). + // ========================================================================= + + syntax List ::= #toKeyAndIsSignerList( List ) [function] + // ------------------------------------------------------------- + rule #toKeyAndIsSignerList(.List) => .List + rule #toKeyAndIsSignerList( + ListItem(Aggregate(variantIdx(0), + ListItem(_) ListItem(Integer(IS, 8, false)) + ListItem(_) ListItem(_) ListItem(_) + ListItem(KEY) ListItem(_) ListItem(_) ListItem(_))) + REST) + => ListItem(keyAndIsSigner(KEY, IS)) #toKeyAndIsSignerList(REST) + endmodule ``` @@ -375,213 +392,135 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA andBool OWNER_OF_ACCOUNT ==K #programIdKey [priority(30)] + // ========================================================================= + // Evaluate tx_signer accounts via manual heating/cooling. + // Walks the Range pointer list, evaluates each tx_signer account one at a + // time, and collects the resulting Values into a list. + // ========================================================================= + syntax KItem ::= #resolveSignerCountExpected( Int, List, // M, REGS (already-sliced registered keys) - Evaluation, - Place, + Evaluation, // deref'd slice (evaluates to Range value) + Place, // original tx_signers Place Place, MaybeBasicBlockIdx ) [seqstrict(3)] - rule [resolve-3-signers-expected]: - #resolveSignerCountExpected( - M, REGS, - Range(ListItem(_) ListItem(_) ListItem(_)), - place(LOCAL2, PROJS2), - DEST, TARGET) - => #checkSigners3Expected( - M, REGS, - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 3)))), - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 3)))), - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(2, 3)))), - DEST, TARGET) - - [priority(30)] - - rule [resolve-2-signers-expected]: + // After the Range is evaluated, start the eval loop. + rule [resolve-signers-expected-start]: #resolveSignerCountExpected( M, REGS, - Range(ListItem(_) ListItem(_)), + Range(PTRS), place(LOCAL2, PROJS2), DEST, TARGET) - => #checkSigners2Expected( - M, REGS, - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 2)))), - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 2)))), - DEST, TARGET) - - [priority(30)] - - rule [resolve-1-signer-expected]: - #resolveSignerCountExpected( + => #evalTxSignersExpected( M, REGS, - Range(ListItem(_)), + 0, size(PTRS), + PTRS, + .List, place(LOCAL2, PROJS2), DEST, TARGET) - => #checkSigners1Expected( - M, REGS, - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 1)))), - DEST, TARGET) [priority(30)] - // --- 3 tx_signers --- - // After evaluating the 3 tx_signer accounts, use generic list-based helpers. - - syntax KItem ::= #checkSigners3Expected( + syntax KItem ::= #evalTxSignersExpected( Int, List, // M, REGS - Evaluation, Evaluation, Evaluation, - Place, MaybeBasicBlockIdx - ) [seqstrict(3,4,5)] - - rule [validate-owner-expected-multisig-unsigned-3]: - #checkSigners3Expected( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), - DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) - - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) - [priority(30)] + Int, Int, // I (current index), N (total tx_signers) + List, // remaining pointers + List, // accumulator of evaluated Values + Place, // original tx_signers Place + Place, MaybeBasicBlockIdx ) - rule [validate-owner-expected-multisig-not-enough-3]: - #checkSigners3Expected( + syntax KItem ::= #evalTxSignersExpectedCont( + Int, List, // M, REGS + Int, Int, // I+1, N + List, // remaining pointers + List, // accumulator + Place, // original tx_signers Place + Place, MaybeBasicBlockIdx ) + + // Heat: evaluate the I-th tx_signer account. + rule [eval-tx-signer-expected-heat]: + #evalTxSignersExpected( M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + I, N, + ListItem(_) REST, + ACC, + place(LOCAL2, PROJS2), DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) - - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) #checkSigners3Expected( + => operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(I, N)))) + ~> #evalTxSignersExpectedCont( M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + I +Int 1, N, + REST, + ACC, + place(LOCAL2, PROJS2), DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) >=Int M [priority(30)] - // --- 2 tx_signers --- - - syntax KItem ::= #checkSigners2Expected( - Int, List, // M, REGS - Evaluation, Evaluation, - Place, MaybeBasicBlockIdx - ) [seqstrict(3,4)] - - rule [validate-owner-expected-multisig-unsigned-2]: - #checkSigners2Expected( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + // Cool: collect the evaluated Value into the accumulator. + rule [eval-tx-signer-expected-cool]: + VAL:Value + ~> #evalTxSignersExpectedCont( + M, REGS, + I, N, + REST, + ACC, + PLACE, DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) - - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) - [priority(30)] - - rule [validate-owner-expected-multisig-not-enough-2]: - #checkSigners2Expected( + => #evalTxSignersExpected( M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + I, N, + REST, + ACC ListItem(VAL), + PLACE, DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) #checkSigners2Expected( + // Done: all tx_signers evaluated, check signatures. + rule [eval-tx-signers-expected-done]: + #evalTxSignersExpected( M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), + _I, _N, + .List, + ACC, + _PLACE, DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) + => #checkSignersExpected(M, REGS, #toKeyAndIsSignerList(ACC), DEST, TARGET) - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) >=Int M [priority(30)] - // --- 1 tx_signer --- + // ========================================================================= + // Generic signer checking (cases 8-10) for expected_validate_owner_result. + // ========================================================================= - syntax KItem ::= #checkSigners1Expected( + syntax KItem ::= #checkSignersExpected( Int, List, // M, REGS - Evaluation, - Place, MaybeBasicBlockIdx - ) [seqstrict(3)] + List, // tx_signers as keyAndIsSigner pairs + Place, MaybeBasicBlockIdx ) - rule [validate-owner-expected-multisig-unsigned-1]: - #checkSigners1Expected( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) + rule [validate-owner-expected-multisig-unsigned]: + #checkSignersExpected(_M, REGS, TXSIGNERS, DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) + requires #unsignedExists(TXSIGNERS, REGS) [priority(30)] - rule [validate-owner-expected-multisig-not-enough-1]: - #checkSigners1Expected( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) + rule [validate-owner-expected-multisig-not-enough]: + #checkSignersExpected(M, REGS, TXSIGNERS, DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List)))) ~> #continueAt(TARGET) // Err(MissingRequiredSignature) - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) #checkSigners1Expected( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) + rule [validate-owner-expected-multisig-ok]: + #checkSignersExpected(M, REGS, TXSIGNERS, DEST, TARGET) + => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) >=Int M + requires notBool #unsignedExists(TXSIGNERS, REGS) + andBool #signersCount(TXSIGNERS, REGS) >=Int M [priority(30)] endmodule @@ -967,333 +906,181 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA andBool OWNER_OF_ACCOUNT ==K #programIdKey [priority(30)] + // ========================================================================= + // Evaluate tx_signer accounts via manual heating/cooling. + // Same structure as the Expected module, but carries RESULT for assertions. + // ========================================================================= + syntax KItem ::= #resolveSignerCount( Int, List, // M, REGS (already-sliced registered keys) - Evaluation, // 3: deref'd slice (evaluates to array value) - Place, // 4: original tx_signers Place - Value, // 5: RESULT + Evaluation, // deref'd slice (evaluates to Range value) + Place, // original tx_signers Place + Value, // RESULT Place, MaybeBasicBlockIdx ) [seqstrict(3)] - // Dispatch: 3 tx_signers - rule [resolve-3-signers]: + // After the Range is evaluated, start the eval loop. + rule [resolve-signers-start]: #resolveSignerCount( M, REGS, - Range(ListItem(_) ListItem(_) ListItem(_)), + Range(PTRS), place(LOCAL2, PROJS2), RESULT, DEST, TARGET) - => #checkSigners3( + => #evalTxSigners( M, REGS, - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 3)))), - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 3)))), - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(2, 3)))), + 0, size(PTRS), + PTRS, + .List, + place(LOCAL2, PROJS2), RESULT, DEST, TARGET) [priority(30)] - // Dispatch: 2 tx_signers - rule [resolve-2-signers]: - #resolveSignerCount( + syntax KItem ::= #evalTxSigners( + Int, List, // M, REGS + Int, Int, // I (current index), N (total tx_signers) + List, // remaining pointers + List, // accumulator of evaluated Values + Place, // original tx_signers Place + Value, // RESULT + Place, MaybeBasicBlockIdx ) + + syntax KItem ::= #evalTxSignersCont( + Int, List, // M, REGS + Int, Int, // I+1, N + List, // remaining pointers + List, // accumulator + Place, // original tx_signers Place + Value, // RESULT + Place, MaybeBasicBlockIdx ) + + // Heat: evaluate the I-th tx_signer account. + rule [eval-tx-signer-heat]: + #evalTxSigners( M, REGS, - Range(ListItem(_) ListItem(_)), + I, N, + ListItem(_) REST, + ACC, place(LOCAL2, PROJS2), RESULT, DEST, TARGET) - => #checkSigners2( + => operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(I, N)))) + ~> #evalTxSignersCont( M, REGS, - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 2)))), - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(1, 2)))), + I +Int 1, N, + REST, + ACC, + place(LOCAL2, PROJS2), RESULT, DEST, TARGET) [priority(30)] - // Dispatch: 1 tx_signer - rule [resolve-1-signer]: - #resolveSignerCount( + // Cool: collect the evaluated Value into the accumulator. + rule [eval-tx-signer-cool]: + VAL:Value + ~> #evalTxSignersCont( M, REGS, - Range(ListItem(_)), - place(LOCAL2, PROJS2), + I, N, + REST, + ACC, + PLACE, RESULT, DEST, TARGET) - => #checkSigners1( + => #evalTxSigners( + M, REGS, + I, N, + REST, + ACC ListItem(VAL), + PLACE, + RESULT, + DEST, TARGET) + + [priority(30)] + + // Done: all tx_signers evaluated, check signatures. + rule [eval-tx-signers-done]: + #evalTxSigners( M, REGS, - operandCopy(place(LOCAL2, appendP(PROJS2, #txSignerAccountProjs(0, 1)))), + _I, _N, + .List, + ACC, + _PLACE, RESULT, DEST, TARGET) + => #checkSigners(M, REGS, #toKeyAndIsSignerList(ACC), RESULT, DEST, TARGET) [priority(30)] // ========================================================================= - // 3 tx_signers: #checkSigners3 - // Uses generic list-based #unsignedExists and #signersCount helpers. + // Generic signer checking (cases 8-10) for inner_test_validate_owner. + // Each case has pass/fail rule pairs for the assert_eq! check. // ========================================================================= - syntax KItem ::= #checkSigners3( + syntax KItem ::= #checkSigners( Int, List, // M, REGS - Evaluation, Evaluation, Evaluation, - Value, // 6: RESULT - Place, MaybeBasicBlockIdx - ) [seqstrict(3,4,5)] + List, // tx_signers as keyAndIsSigner pairs + Value, // RESULT + Place, MaybeBasicBlockIdx ) // Case 8: unsigned signer exists => assert result == Err(MissingRequiredSignature) - rule [inner-validate-owner-multisig-unsigned-3]: - #checkSigners3( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + rule [inner-validate-owner-multisig-unsigned]: + #checkSigners( + _M, REGS, TXSIGNERS, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, DEST, TARGET) => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) + requires #unsignedExists(TXSIGNERS, REGS) [priority(30)] - rule [inner-validate-owner-multisig-unsigned-3-fail]: - #checkSigners3( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + rule [inner-validate-owner-multisig-unsigned-fail]: + #checkSigners( + _M, REGS, TXSIGNERS, RESULT, _DEST, _TARGET) => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) + requires #unsignedExists(TXSIGNERS, REGS) andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) [priority(30)] // Case 9: not enough signers => assert result == Err(MissingRequiredSignature) - rule [inner-validate-owner-multisig-not-enough-3]: - #checkSigners3( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + rule [inner-validate-owner-multisig-not-enough]: + #checkSigners( + M, REGS, TXSIGNERS, Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, DEST, TARGET) => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) #checkSigners3( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + rule [inner-validate-owner-multisig-not-enough-fail]: + #checkSigners( + M, REGS, TXSIGNERS, RESULT, _DEST, _TARGET) => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) Ok(()) (no assert on result) - rule [inner-validate-owner-multisig-ok-3]: - #checkSigners3( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS2, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY2) ListItem(_) ListItem(_) ListItem(_)), + rule [inner-validate-owner-multisig-ok]: + #checkSigners( + M, REGS, TXSIGNERS, _RESULT, DEST, TARGET) => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) // Ok(()) - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)) ListItem(keyAndIsSigner(KEY2, IS2)), - REGS) >=Int M - [priority(30)] - - // --- 2 tx_signers --- - - syntax KItem ::= #checkSigners2( - Int, List, // M, REGS - Evaluation, Evaluation, - Value, // 5: RESULT - Place, MaybeBasicBlockIdx - ) [seqstrict(3,4)] - - rule [inner-validate-owner-multisig-unsigned-2]: - #checkSigners2( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, - DEST, TARGET) - => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) - [priority(30)] - - rule [inner-validate-owner-multisig-unsigned-2-fail]: - #checkSigners2( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - RESULT, _DEST, _TARGET) - => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) - andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) - [priority(30)] - - rule [inner-validate-owner-multisig-not-enough-2]: - #checkSigners2( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, - DEST, TARGET) - => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) #checkSigners2( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - RESULT, _DEST, _TARGET) - => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) #checkSigners2( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS1, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY1) ListItem(_) ListItem(_) ListItem(_)), - _RESULT, DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) - - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)) ListItem(keyAndIsSigner(KEY1, IS1)), - REGS) >=Int M - [priority(30)] - - // --- 1 tx_signer --- - - syntax KItem ::= #checkSigners1( - Int, List, // M, REGS - Evaluation, - Value, // 4: RESULT - Place, MaybeBasicBlockIdx - ) [seqstrict(3)] - - rule [inner-validate-owner-multisig-unsigned-1]: - #checkSigners1( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, - DEST, TARGET) - => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) - [priority(30)] - - rule [inner-validate-owner-multisig-unsigned-1-fail]: - #checkSigners1( - _M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - RESULT, _DEST, _TARGET) - => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - - requires #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) - andBool RESULT =/=K Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) - [priority(30)] - - rule [inner-validate-owner-multisig-not-enough-1]: - #checkSigners1( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))) #as RESULT, - DEST, TARGET) - => #setLocalValue(DEST, RESULT) ~> #continueAt(TARGET) - - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) #checkSigners1( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - RESULT, _DEST, _TARGET) - => #ValidateOwnerAssertFailed(Result2String(RESULT) +String " =/= " +String Result2String(Aggregate(variantIdx(1), ListItem(Aggregate(variantIdx(7), .List))))) - - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) #checkSigners1( - M, REGS, - Aggregate(variantIdx(0), ListItem(_) ListItem(Integer(IS0, 8, false)) ListItem(_) ListItem(_) ListItem(_) ListItem(KEY0) ListItem(_) ListItem(_) ListItem(_)), - _RESULT, DEST, TARGET) - => #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List)))) ~> #continueAt(TARGET) - - requires notBool #unsignedExists( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) - andBool #signersCount( - ListItem(keyAndIsSigner(KEY0, IS0)), - REGS) >=Int M + requires notBool #unsignedExists(TXSIGNERS, REGS) + andBool #signersCount(TXSIGNERS, REGS) >=Int M [priority(30)] endmodule From 5653cedda59efb3ab01aabfc95a206d3cd9a7606 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Mon, 23 Mar 2026 21:58:36 -0500 Subject: [PATCH 7/8] Documentation and renaming. --- .../symbolic/inner_test_validate_owner.md | 164 ++++++++++++++++-- 1 file changed, 151 insertions(+), 13 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md index 6b064cd86..ea2da55b2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md @@ -1,3 +1,140 @@ +# Lemma rules for `expected_validate_owner_result` and `inner_test_validate_owner` + +## Overview + +These lemma modules summarize two functions from the test harness +(`specs/shared/inner_test_validate_owner.rs`) that specify the expected behavior +of `validate_owner` in the SPL Token program. Instead of letting the K prover +symbolically execute these functions step-by-step (which produces hundreds of +splits from nested iterator loops), the lemma rules intercept each function call +and directly produce the result in a single rewrite step. + +Both functions implement the same case analysis over the `validate_owner` logic. +The difference is that `expected_validate_owner_result` computes and returns the +expected `Result<(), ProgramError>`, while `inner_test_validate_owner` takes an +additional `result` parameter and asserts (`assert_eq!`) that it matches the +expected outcome at each error branch. + +## Case analysis + +The branching structure follows the Rust code in `expected_validate_owner_result` +(and identically in `inner_test_validate_owner`): + +| Case | Condition | Result | +|------|-----------|--------| +| 1 | `expected_owner != key!(owner_account_info)` | `Err(Custom(4))` | +| 2 | owner matches, non-multisig, `!is_signer` | `Err(MissingRequiredSignature)` | +| 3 | owner matches, non-multisig, `is_signer` | `Ok(())` | +| 4 | owner matches, multisig, `owner != PROGRAM_ID`, `!is_signer` | `Err(MissingRequiredSignature)` | +| 5 | owner matches, multisig, `owner != PROGRAM_ID`, `is_signer` | `Ok(())` | +| 6 | owner matches, multisig, `owner == PROGRAM_ID`, `is_initialized()` returns `Err` | `Err(InvalidAccountData)` | +| 7 | owner matches, multisig, `owner == PROGRAM_ID`, `is_initialized()` returns `Ok(false)` | `Err(UninitializedAccount)` | +| 8 | owner matches, multisig, `owner == PROGRAM_ID`, initialized, `unsigned_exists` | `Err(MissingRequiredSignature)` | +| 9 | owner matches, multisig, `owner == PROGRAM_ID`, initialized, `!unsigned_exists`, `signers_count < m` | `Err(MissingRequiredSignature)` | +| 10 | owner matches, multisig, `owner == PROGRAM_ID`, initialized, `!unsigned_exists`, `signers_count >= m` | `Ok(())` | + +Cases 1-3 apply when `maybe_multisig_is_initialised` is `None` (non-multisig +path, used by `test_validate_owner`). Case 1 also applies to the multisig path +since the owner check happens first regardless. + +Cases 4-5 are the multisig fallthrough: the account was passed as a multisig +(`maybe_multisig_is_initialised` is `Some(...)`) but its `owner` field does not +equal `PROGRAM_ID`, so the multisig signer-checking is skipped and the code +falls through to the simple `is_signer` check. + +Cases 6-7 are multisig early exits based on the `is_initialized()` result +(which comes from the `is_initialized` field of the `Multisig` struct: 0 means +`Ok(false)`, 1 means `Ok(true)`, anything else means `Err(InvalidAccountData)`). + +Cases 8-10 are the multisig signer-checking phase, which involves two nested +loops over tx_signers (transaction signer accounts from the input array) and +`multisig.signers[0..n]` (the first `n` registered signer keys). The loop +nesting order differs between the two checks: + +- **`unsigned_exists`** (case 8): outer loop over tx_signers, inner loop over + registered keys. True if any tx_signer matches a registered key but has + `is_signer == false`. +- **`signers_count`** (cases 9-10): outer loop over registered keys, inner loop + over tx_signers. Counts how many registered keys have a matching signed + tx_signer. + +Cases 9 and 10 are only reachable when `unsigned_exists` is false (no unsigned +signer matched a registered key). Case 9 then checks if `signers_count < m` +(not enough signatures). Case 10 is the success path where +`signers_count >= m`. + +## Signer-checking helpers + +The signer-checking logic in cases 8-10 uses list-based helper functions +(`#unsignedExists`, `#signersCount`) that work generically over any number of +signers, rather than having separate rules for each combination of tx_signer +count and registered signer count. + +The two dimensions are: +- **`n`** (registered signers, from `multisig.n`): can be 1, 2, or 3 (bounded + by `MAX_SIGNERS = 3`). Handled by matching `U8(N)` concretely in the + `IMulti` pattern and using `firstN(N, SKEYS)` to slice the registered keys. +- **tx_signer count** (from the test input array size): any number. Handled + generically by manual heating/cooling rules that walk the `Range` pointer + list, evaluate each tx_signer account one at a time, and collect the results + into a `List`. The `#toKeyAndIsSignerList` function then extracts key and + is_signer fields from each evaluated account. No new rules are needed when + the tx_signer count changes. + +Both values of `n` and the tx_signer count are independent — any combination is +handled. + +`n` is matched concretely (not passed as a symbolic argument) because when `n` +is symbolic, `firstN` produces non-deterministic branches and a stuck node that +the prover cannot prune. + +`m` (the threshold) remains symbolic throughout and is only used in the final +comparison `#signersCount(...) =Int M`. + +## Heating/cooling for tx_signer evaluation + +The tx_signer accounts are evaluated using manual heating/cooling rather than +`seqstrict`. This is because `seqstrict` only works on fixed positional +arguments of a syntax term, not on elements of a `List`. Manual heating/cooling +walks the `Range` pointer list, evaluates each tx_signer account one at a time +via `operandCopy`, and collects the resulting `Value`s into a `List`. This makes +the tx_signer count fully generic — no dispatch rules per count. + +The tx_signer count is always concrete (it comes from the test harness array +size), unlike `n` which is symbolic. So there is no risk of non-deterministic +branching. + +Each lemma module has its own heating/cooling loop (`#evalTxSignersExpected` / +`#evalTxSigners`) because the `inner_test_validate_owner` version carries an +additional `RESULT` parameter. The shared `#toKeyAndIsSignerList` function in +`VALIDATE-OWNER-COMMON` handles the extraction step separately. + +## Module structure + +- **`VALIDATE-OWNER-COMMON`**: shared helpers — `Result2String`, `#programIdKey`, + `#txSignerAccountProjs`, `#bool2Int`, `firstN`, `#unsignedExists`, + `#signersCount`, `keyAndIsSigner`, `#toKeyAndIsSignerList`. +- **`EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA`**: intercepts + `expected_validate_owner_result` (4 arguments), directly returns the result. +- **`INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA`**: intercepts + `inner_test_validate_owner` (5 arguments, includes `result` parameter). Error + cases have pass/fail rule pairs; success cases return `Ok(())` without + asserting. + +## `inner_test_validate_owner` pass/fail rules + +For each error case (1, 2, 4, 6, 7, 8, 9), the `inner_test_validate_owner` +lemma has two rules: +- **Pass**: the `result` argument matches the expected error value (bound with + `#as RESULT`), so the rule returns it via `#setLocalValue(DEST, RESULT)`. +- **Fail**: the `result` argument does not match, so the rule produces + `#ValidateOwnerAssertFailed(...)` with a diagnostic message showing the + mismatch. + +For the success cases (3, 5, 10), there is no assertion on `result` — the rule +unconditionally returns `Ok(())`, matching the Rust code which does not call +`assert_eq!` on the success path. + ```k requires "../kmir-ast.md" requires "../rt/data.md" @@ -82,7 +219,8 @@ module VALIDATE-OWNER-COMMON // Generic signer checking helpers (list-based) // // These work for any number of tx_signers and registered signers. - // The caller constructs lists from the extracted values. + // The heating/cooling loop collects evaluated account Values into a list, + // then #toKeyAndIsSignerList extracts key/is_signer pairs for these helpers. // // keyAndIsSigner(KEY, IS) pairs a tx_signer's public key with its is_signer flag. // firstN(N, LIST) takes the first N elements of LIST (implements [0..n] slicing). @@ -166,7 +304,7 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA imports VALIDATE-OWNER-COMMON // ========================================================================= - // Intercept rule and dispatch helper + // Intercept rule // ========================================================================= syntax KItem ::= #validateOwnerResultExpected( Evaluation, Evaluation, Place, Evaluation, Place, MaybeBasicBlockIdx ) @@ -336,7 +474,7 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA Aggregate(variantIdx(0), ListItem( BoolVal(true))))), // Some(Ok(true)) DEST, TARGET) - => #resolveSignerCountExpected( + => #evalTxSignerAccountsExpected( M, SKEYS, operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), place(LOCAL2, PROJS2), @@ -359,7 +497,7 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA Aggregate(variantIdx(0), ListItem( BoolVal(true))))), // Some(Ok(true)) DEST, TARGET) - => #resolveSignerCountExpected( + => #evalTxSignerAccountsExpected( M, firstN(2, SKEYS), operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), place(LOCAL2, PROJS2), @@ -382,7 +520,7 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA Aggregate(variantIdx(0), ListItem( BoolVal(true))))), // Some(Ok(true)) DEST, TARGET) - => #resolveSignerCountExpected( + => #evalTxSignerAccountsExpected( M, firstN(1, SKEYS), operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), place(LOCAL2, PROJS2), @@ -398,7 +536,7 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA // time, and collects the resulting Values into a list. // ========================================================================= - syntax KItem ::= #resolveSignerCountExpected( + syntax KItem ::= #evalTxSignerAccountsExpected( Int, List, // M, REGS (already-sliced registered keys) Evaluation, // deref'd slice (evaluates to Range value) Place, // original tx_signers Place @@ -407,7 +545,7 @@ module EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA // After the Range is evaluated, start the eval loop. rule [resolve-signers-expected-start]: - #resolveSignerCountExpected( + #evalTxSignerAccountsExpected( M, REGS, Range(PTRS), place(LOCAL2, PROJS2), @@ -538,7 +676,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA imports VALIDATE-OWNER-COMMON // ========================================================================= - // Intercept rule and dispatch helper + // Intercept rule // ========================================================================= // // inner_test_validate_owner has 5 arguments: @@ -845,7 +983,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA BoolVal(true))))), // Some(Ok(true)) RESULT, DEST, TARGET) - => #resolveSignerCount( + => #evalTxSignerAccounts( M, SKEYS, operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), place(LOCAL2, PROJS2), @@ -870,7 +1008,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA BoolVal(true))))), // Some(Ok(true)) RESULT, DEST, TARGET) - => #resolveSignerCount( + => #evalTxSignerAccounts( M, firstN(2, SKEYS), operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), place(LOCAL2, PROJS2), @@ -895,7 +1033,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA BoolVal(true))))), // Some(Ok(true)) RESULT, DEST, TARGET) - => #resolveSignerCount( + => #evalTxSignerAccounts( M, firstN(1, SKEYS), operandCopy(place(LOCAL2, appendP(PROJS2, projectionElemDeref .ProjectionElems))), place(LOCAL2, PROJS2), @@ -911,7 +1049,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA // Same structure as the Expected module, but carries RESULT for assertions. // ========================================================================= - syntax KItem ::= #resolveSignerCount( + syntax KItem ::= #evalTxSignerAccounts( Int, List, // M, REGS (already-sliced registered keys) Evaluation, // deref'd slice (evaluates to Range value) Place, // original tx_signers Place @@ -921,7 +1059,7 @@ module INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA // After the Range is evaluated, start the eval loop. rule [resolve-signers-start]: - #resolveSignerCount( + #evalTxSignerAccounts( M, REGS, Range(PTRS), place(LOCAL2, PROJS2), From 518ed56ee45afc07935a3233eda034267cdc0385 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Tue, 24 Mar 2026 09:52:47 -0500 Subject: [PATCH 8/8] Commenting out lemmas for default. --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index a3bd623fe..7c5680282 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -10,7 +10,7 @@ requires "intrinsics.md" requires "symbolic/p-token.md" requires "symbolic/spl-token.md" -requires "symbolic/inner_test_validate_owner.md" +// requires "symbolic/inner_test_validate_owner.md" ``` ## Syntax of MIR in K @@ -720,7 +720,7 @@ module KMIR imports KMIR-P-TOKEN // cheat codes imports KMIR-SPL-TOKEN // SPL-specific cheat codes - imports EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA - imports INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA + // imports EXPECTED-VALIDATE-OWNER-RESULT-P-TOKEN-LEMMA + // imports INNER-TEST-VALIDATE-OWNER-P-TOKEN-LEMMA endmodule ```