// VeriFast-annotated partial JavaCard API
// Status:
// - Should be sound, even in the presence of card tearing. That is, during all executions of verified programs, all assert statements succeed.
// - Not all API method preconditions specified in the official API docs have been encoded yet; this means an execution of a verified program may throw exceptions
// TODO:
// - Strengthen contracts so that in executions of a verified program, API calls do not throw exceptions
// - Support transient objects (i.e. the JCSystem.makeTransientXXX methods). (This requires keeping track of them and consuming them during register() and commitTransaction() to ensure they do not end up in applet.valid().)
// - Support JCSystem.abortTransaction(). (This is difficult because the footprint of this method is all persistent objects modified during the transaction, which might include objects not in currentApplet.valid().)
// - Support communication with other applets.

package javacard.framework;

/*@

fixpoint boolean is_persistent_object(Object o);

predicate APDU(APDU apdu, byte[] buffer);

lemma_auto void APDU_inv();
    requires APDU(?apdu, ?buffer);
    ensures APDU(apdu, buffer) &*& apdu != null &*& buffer != null &*& !is_persistent_object(buffer) &*& 133 <= buffer.length;

@*/

class APDU {
    public byte[] getBuffer();
        //@ requires APDU(this, ?buffer);
        //@ ensures APDU(this, buffer) &*& result == buffer;
    
    public short setOutgoing() throws APDUException;
        //@ requires APDU(this, ?buffer) &*& array_slice(buffer, 0, buffer.length, _);
        //@ ensures APDU(this, buffer) &*& array_slice(buffer, 0, buffer.length, _);
    
    public short setIncomingAndReceive() throws APDUException;
        //@ requires APDU(this, ?buffer) &*& array_slice(buffer, 0, buffer.length, _);
        //@ ensures APDU(this, buffer) &*& array_slice(buffer, 0, buffer.length, _);
    
    public void setOutgoingAndSend(short bOff, short len) throws APDUException;
        //@ requires APDU(this, ?buffer) &*& array_slice(buffer, 0, buffer.length, _);
        //@ ensures APDU(this, buffer) &*& array_slice(buffer, 0, buffer.length, _);
    
    public void setOutgoingLength(short len) throws APDUException;
        //@ requires APDU(this, ?buffer) &*& array_slice(buffer, 0, buffer.length, _);
        //@ ensures APDU(this, buffer) &*& array_slice(buffer, 0, buffer.length, _);
    
    public void sendBytes(short bOff, short len) throws APDUException;
        //@ requires APDU(this, ?buffer) &*& array_slice(buffer, 0, buffer.length, _);
        //@ ensures APDU(this, buffer) &*& array_slice(buffer, 0, buffer.length, _);
    
    public void sendBytesLong(byte[] outData, short bOff, short len) throws APDUException, SecurityException;
        //@ requires APDU(this, ?buffer) &*& array_slice(buffer, 0, buffer.length, _) &*& outData != null &*& [?f]array_slice(outData, bOff, bOff + len, ?elems);
        //@ ensures APDU(this, buffer) &*& array_slice(buffer, 0, buffer.length, _) &*& outData != null &*& [f]array_slice(outData, bOff, bOff + len, elems);
}

//@ predicate current_applet(Applet applet);

class Applet {
    //@ predicate valid() = false;
    
    public Applet();
        //@ requires true;
        //@ ensures true;
    
    public boolean selectingApplet();
        //@ requires true;
        //@ ensures true;
    
    public void register();
        //@ requires this.valid();
        //@ ensures true;
    
    public void register(byte[] bArray, short bOffset, byte bLength) throws SystemException;
        //@ requires this.valid();
        //@ ensures true;
    
    public boolean select();
        //@ requires current_applet(this) &*& [1/2]this.valid();
        //@ ensures current_applet(this) &*& [1/2]this.valid();
    
    public void deselect();
        //@ requires current_applet(this) &*& [1/2]this.valid();
        //@ ensures current_applet(this) &*& [1/2]this.valid();
    
    public void process(APDU apdu);
        //@ requires current_applet(this) &*& [1/2]valid() &*& APDU(apdu, ?buffer) &*& array_slice(buffer, 0, buffer.length, _);
        //@ ensures current_applet(this) &*& [1/2]valid() &*& APDU(apdu, buffer) &*& array_slice(buffer, 0, buffer.length, _);
}

class ISOException {
    public static void throwIt(short sw) throws ISOException;
        //@ requires true;
        //@ ensures false;
}

class OPSystem {
    public static final byte APPLET_BLOCKED = 127;
    public static final byte APPLET_PERSONALIZED = 15;
    public static final byte APPLET_INSTALLED = 3;
    public static final byte APPLET_SELECTABLE = 7;
    public static final byte APPLET_LOCKED = -1;
    public static final byte CARD_INITIALIZED = 7;
    public static final byte INITIALIZED = 7;
    public static final byte CARD_SECURED = 15;
    public static final byte CARD_LOCKED = 127;
    public static final byte CARD_OP_READY = 1;
    public static final byte PACKAGE_LOADED = 1;
    
    public static byte getCardContentState();
        //@ requires true;
        //@ ensures true;
    
    public static boolean setCardContentState(byte state);
        //@ requires true;
        //@ ensures true;
}

class AID {
}

class JCSystem {
    public static AID lookupAID(byte[] buffer, short offset, byte length);
        //@ requires [?f]array_slice(buffer, offset, offset + length, ?elems);
        //@ ensures [f]array_slice(buffer, offset, offset + length, elems);
    
    public static void beginTransaction();
        //@ requires current_applet(?applet);
        //@ ensures current_applet(applet) &*& [1/2]applet.valid();
    
    // It's crucial for soundness that commitTransaction() consumes the full applet.valid() chunk. Consuming only [1/2]applet.valid() is unsound.
    // E.g.: predicate valid() = x |-> ?b &*& b ? y |-> _ : [2]y |-> _;
    //       In process(), set b = false, then commit, then throw an exception. Next time you enter process(), you have [1]y |-> _ outside a transaction.
    public static void commitTransaction();
        //@ requires current_applet(?applet) &*& applet.valid();
        //@ ensures current_applet(applet) &*& [1/2]applet.valid();
}

class Util {
    public static final byte arrayCompare(byte[] src, short srcOff, byte[] dest, short destOff, short length);
        //@ requires [?f1]array_slice(src, srcOff, srcOff + length, ?elems1) &*& [?f2]array_slice(dest, destOff, destOff + length, ?elems2);
        //@ ensures [f1]array_slice(src, srcOff, srcOff + length, elems1) &*& [f2]array_slice(dest, destOff, destOff + length, elems2);
    
    public static short arrayCopyNonAtomic(byte[] src, short srcOff, byte[] dest, short destOff, short length)
        throws ArrayIndexOutOfBoundsException;
        //@ requires [?f]array_slice(src, srcOff, srcOff + length, ?elems) &*& array_slice(dest, destOff, destOff + length, _) &*& !is_persistent_object(dest);
        //@ ensures [f]array_slice(src, srcOff, srcOff + length, elems) &*& array_slice(dest, destOff, destOff + length, elems) &*& result == destOff + length;
      
    public static final short arrayCopy(byte[] src, short srcOff, byte[] dest, short destOff, short length);
        //@ requires [?f]array_slice(src, srcOff, srcOff + length, ?elems) &*& array_slice(dest, destOff, destOff + length, _);
        //@ ensures [f]array_slice(src, srcOff, srcOff + length, elems) &*& array_slice(dest, destOff, destOff + length, elems) &*& result == destOff + length;
    
    public static final short getShort(byte[] bArray, short bOff) throws NullPointerException, ArrayIndexOutOfBoundsException;
        //@ requires [?f]array_slice(bArray, bOff, bOff + 2, ?elems);
        //@ ensures [f]array_slice(bArray, bOff, bOff + 2, elems);
}

class ISO7816 {
    public static final byte CLA_ISO7816 = 0x00;
    public static final byte INS_EXTERNAL_AUTHENTICATE = (byte) 0x82;
    public static final byte INS_SELECT = (byte) 0xA4;
    public static final byte OFFSET_CDATA = 5;
    public static final byte OFFSET_CLA = 0;
    public static final byte OFFSET_EXT_CDATA = 7;
    public static final byte OFFSET_INS = 1;
    public static final byte OFFSET_LC = 4;
    public static final byte OFFSET_P1 = 2;
    public static final byte OFFSET_P2 = 3;
    
    public static final short SW_APPLET_SELECT_FAILED = (short) 0x6999;
    public static final short SW_BYTES_REMAINING_00 = (short) 0x6100;
    public static final short SW_CLA_NOT_SUPPORTED = (short) 0x6E00;
    public static final short SW_COMMAND_CHAINING_NOT_SUPPORTED = (short) 0x6884;
    public static final short SW_COMMAND_NOT_ALLOWED = (short) 0x6986;
    public static final short SW_CONDITIONS_NOT_SATISFIED = (short) 0x6985;
    public static final short SW_CORRECT_LENGTH_00 = (short) 0x6C00;
    public static final short SW_DATA_INVALID = (short) 0x6984;
    public static final short SW_FILE_FULL = (short) 0x6A84;
    public static final short SW_FILE_INVALID = (short) 0x6983;
    public static final short SW_FILE_NOT_FOUND = (short) 0x6A82;
    public static final short SW_FUNC_NOT_SUPPORTED = (short) 0x6A81;
    public static final short SW_INCORRECT_P1P2 = (short) 0x6A86;
    public static final short SW_INS_NOT_SUPPORTED = (short) 0x6D00;
    public static final short SW_LAST_COMMAND_EXPECTED = (short) 0x6883;
    public static final short SW_LOGICAL_CHANNEL_NOT_SUPPORTED = (short) 0x6881;
    public static final short SW_NO_ERROR = (short) 0x9000;
    public static final short SW_RECORD_NOT_FOUND = (short) 0x6A83;
    public static final short SW_SECURE_MESSAGING_NOT_SUPPORTED = (short) 0x6882;
    public static final short SW_SECURITY_STATUS_NOT_SATISFIED = (short) 0x6982;
    public static final short SW_UNKNOWN = (short) 0x6F00;
    public static final short SW_WARNING_STATE_UNCHANGED = (short) 0x6200;
    public static final short SW_WRONG_DATA = (short) 0x6A80;
    public static final short SW_WRONG_LENGTH = (short) 0x6700;
    public static final short SW_WRONG_P1P2 = (short) 0x6B00;
}