Remove summary apply bitvector

safe-global · May 29, 2024 · 1a90bed · 1a90bed
1 parent caf2a10
commit 1a90bed
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 41 deletions.
diff --git a/certora/harnesses/WebAuthnHarness.sol b/certora/harnesses/WebAuthnHarness.sol
@@ -4,23 +4,6 @@ pragma solidity ^0.8.0;
 import {P256, WebAuthn} from "../../modules/passkey/contracts/libraries/WebAuthn.sol";
 
 contract WebAuthnHarness {
-
-    mapping(bytes32 => mapping(bytes32 => string)) summaryMap;
-
-    function getEncodeClientDataJsonSummary(bytes32 message, string calldata signature) public view returns (string memory){
-        bytes32 hashed_signature = keccak256(abi.encodePacked(signature));
-        string memory string_mapping = summaryMap[message][hashed_signature];
-        bytes32 hashed_mapping = keccak256(abi.encodePacked(string_mapping));
-
-        require (encodeAxiom(message, hashed_signature, hashed_mapping));
-
-        return string_mapping;
-    }
-
-    function encodeAxiom(bytes32 message, bytes32 signature, bytes32 result) internal pure returns (bool){
-        return true;
-    }
-
     function compareSignatures(WebAuthn.Signature memory sig1, WebAuthn.Signature memory sig2) public pure returns (bool) {
         if (sig1.r != sig2.r || sig1.s != sig2.s) {
             return false;

diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec
@@ -1,28 +1,9 @@
-methods{
-    function getEncodeClientDataJsonSummary(bytes32 message, string calldata signature) external returns (string memory);
-
-    function WebAuthn.encodeClientDataJson(bytes32 message, string calldata signature) internal returns (string memory) => 
-        getEncodeClientDataJsonSummaryCVL(message, signature);
-
-    function encodeAxiom(bytes32 message, bytes32 signature, bytes32 result) internal returns (bool) =>
-        encodeAxiomSummary(message, signature, result);
-
-    //function encodeSigningMessage(bytes32,bytes calldata,string calldata) internal returns(bytes memory) => NONDET;
-    function castSignature(bytes calldata signature) external returns (bool, WebAuthn.Signature calldata);
-}
-
-function getEncodeClientDataJsonSummaryCVL(bytes32 message, string signature) returns string
-{
-    env e;
-    return getEncodeClientDataJsonSummary(e, message, signature);
-}
 
-ghost encodeAxiomSummary(bytes32, bytes32, bytes32) returns bool {
-    axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 x2. forall bytes32 y2. forall bytes32 z.
-    (x1 != x2 || y1 != y2) => !(encodeAxiomSummary(x1, y1, z) && encodeAxiomSummary(x2, y2, z));
-}
-
-// Inner Check for Summarization
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ encodeClientDataJsonIntegrity 2 different challenges results in 2 different clientDataJson (Violated)               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
 rule encodeClientDataJsonIntegrity(){
 
     env e;