package applet;

import javacard.framework.*;

/**
 * Sample multiplication table applet. Once initialized, a terminal can
 * ask for the entries in the multiplication table: 1 x base, 2 x base,
 * 3 x base, 4 x base, 5 x base, 6 x base, 7 x base, 8 x base, 9 x base,
 * 10 x base.
 *
 * Instructions that are recognized by this applet:
 *    - 0x05: SET BASE takes 1 byte of data to encode new base.
 *    - 0x09: GET NEXT returns 2 bytes of data for next table entry.
 *
 * State consists of:
 *    - the base value (the table of ...),
 *    - a boolean indicating whether the applet's base value is set,
 *    - the current multiplication factor (minus 1) which runs from 0 to 9.
 *
 * Error status words returned by this applet's process method:
 *    - 0x67XX: WRONG LENGTH (length should have been XX)
 *    - 0x6984: DATA INVALID (input data not valid)
 *    - 0x6985: CONDITIONS NOT SATISFIED (wrong state for this command)
 *    - 0x6D00: INS NOT SUPPORTED (unknown instruction)
 */
public class TableApplet extends Applet implements ISO7816 {


   private /*@ spec_public */ static final byte INS_SETBASE = (byte)0x05;
   private /*@ spec_public */ static final byte INS_GETNEXT = (byte)0x09;

   /** Indicates whether this applet has been given an initial base value. */
   private /*@ spec_public */ boolean initialized;

      /* Once initialized, it will stay initialized. */
      /*@ constraint
        @    \old(initialized) ==> initialized;
       */

   /** The base value. This is the table of... */
   private /*@ spec_public */ short base;

      /* If initialized, base is greater than one. */
      /*@ invariant
        @    (!initialized ==> (base == 0)) &&
        @    (initialized ==> (base > 1));
       */

   /** The current multiplication factor (minus 1). */
   private short factor;

      /* The multiplication factor is in 0..9. */
      /*@ invariant
        @    0 <= factor && factor < 10;
       */

      /* The multiplication factor stays the same or grows by 1, modulo 10. */
      /*@ constraint
        @    factor == \old(factor) ||
        @    factor == \old(factor) + 1 ||
        @    (factor == 0 && \old(factor) == 9);
       */

   /*@ 
     @ ensures base == 0 && factor == 9 && !initialized;
     @ signals (SystemException e) e.getReason() == SystemException.ILLEGAL_AID;
    */
   public TableApplet() throws SystemException {
      base = 0;
      factor = 9;
      initialized = false;
      register();
   }

   public static void install(byte[] buffer, short offset, byte length) throws SystemException {
      new TableApplet();
   }

   public boolean select() {
      return true;
   }

   /*@ also
     @ behavior
     @    requires apdu._APDU_state == 1;
     @    requires apdu != null;
     @    assignable base, factor, initialized;
     @    assignable apdu._APDU_state;
     @    assignable apdu._Lc;
     @    assignable apdu._Le;
     @    assignable apdu._Lr;
     @    assignable apdu.buffer[*];
     @    ensures true;
     @    signals (ISOException e) true;
     @    signals (APDUException e) true;
    */
   public void process(APDU apdu) throws ISOException, APDUException {
      byte[] buffer = apdu.getBuffer();
      byte cla = buffer[OFFSET_CLA];
      byte ins = buffer[OFFSET_INS];
      short lc = (short)(buffer[OFFSET_LC] & 0x00FF);
      short le = -1;

      /* Ignore the APDU that selects this applet... */
      if (selectingApplet()) {
         return;
      }
     //@ assert apdu._APDU_state == 1;

      switch (ins) {
         case INS_SETBASE:
            processSetBase(apdu);
            break;
         case INS_GETNEXT:
            processGetNext(apdu);
            break;
         default:
            ISOException.throwIt((short)SW_INS_NOT_SUPPORTED);
      }
   }

   /*@ behavior
     @    requires apdu._APDU_state == 1;
     @    assignable base, initialized;
     @    assignable apdu._APDU_state;
     @    assignable apdu._Lc;
     @    assignable apdu._Le;
     @    assignable apdu.buffer[*];
     @    ensures !\old(initialized) && initialized;
     @    signals (ISOException e) true;
     @    signals (APDUException e) true;
    */
   private void processSetBase(/*@ non_null@*/ APDU apdu) throws ISOException, APDUException {
      byte[] buffer = apdu.getBuffer();
      short lc = (short)(buffer[OFFSET_LC] & 0x00FF);
      if (initialized) {
         ISOException.throwIt(SW_CONDITIONS_NOT_SATISFIED);
      }
      if (lc != 1) {
         ISOException.throwIt((short)(SW_WRONG_LENGTH | 0x0001));
      }
      apdu.setIncomingAndReceive();
      short input = (short)(buffer[OFFSET_CDATA] & 0x00FF);
      if (input <= 1) {
         ISOException.throwIt(SW_DATA_INVALID);
      }
      base = input;
      initialized = true;
   }

   /*@ behavior
     @    requires apdu._APDU_state == 1;
     @    assignable factor;
     @    assignable apdu._APDU_state;
     @    assignable apdu._Le;
     @    assignable apdu._Lr;
     @    assignable apdu.buffer[*];
     @    ensures \old(initialized) && initialized;
     @    signals (ISOException e) factor == \old(factor);
     @    signals (APDUException e) true;
    */
   private void processGetNext(/*@ non_null@*/ APDU apdu) throws ISOException, APDUException {
      byte[] buffer = apdu.getBuffer();
      if (!initialized) {
         ISOException.throwIt(SW_CONDITIONS_NOT_SATISFIED);
      }
      //@ assert initialized;
      //@ assert apdu._APDU_state == 1;
      short le = apdu.setOutgoing();
      //@ assert apdu._APDU_state == 3;
      if (le != 2) {
         ISOException.throwIt((short)(SW_WRONG_LENGTH | 0x0002));
      }
      // factor = (short)((short)(factor + 1) % 10); // Too much for ESC...
      factor = (short)(factor + 1);
      if (factor == 10) factor = (short)0;
      //@ assert 0 <= factor && factor <= 10;
      short value = (short)((short)(factor + 1) * base);
      Util.setShort(buffer,(short)0,value);
      apdu.setOutgoingLength((short)2);
      //@ assert apdu._APDU_state == 4;
      apdu.sendBytes((short)0,(short)2);
      //@ assert apdu._APDU_state == 4;
      //@ assert initialized;
   }
}