content: package xjsnark.sortingVerification;
  
  /*Generated by MPS */
  
  import backend.structure.CircuitGenerator;
  import backend.eval.SampleRun;
  import util.Util;
  import backend.auxTypes.UnsignedInteger;
  import backend.eval.Instruction;
  import backend.eval.CircuitEvaluator;
  import java.math.BigInteger;
  import java.util.Arrays;
  import backend.auxTypes.PermutationVerifier;
  
  public class SortingVerification extends CircuitGenerator {
  
  
  
    public static void main(String[] args) {
      // This is the java main method. Its purpose is to make the Progam runnable in the environment 
      // This method can be left empty, or used to set Configuration params (see examples) 
      new SortingVerification();
    }
  
    public SortingVerification() {
      super("SortingVerification");
      __generateCircuit();
      this.__evaluateSampleRun(new SampleRun("Sample_Run1", true) {
        public void pre() {
          // assign random values to input 
          for (int i = 0; i < SIZE; i++) {
            unsortedArray[i].mapValue(Util.nextRandomBigInteger(16), CircuitGenerator.__getActiveCircuitGenerator().__getCircuitEvaluator());
          }
        }
        public void post() {
          //  elements should be sorted. If sorting in the external block is done wrong, failed assertions will appear 
          for (int i = 0; i < SIZE; i++) {
            System.out.println("Element at " + i + " > " + sortedArray[i].getValueFromEvaluator(CircuitGenerator.__getActiveCircuitGenerator().__getCircuitEvaluator()));
          }
          // disable the print statement above, and 
          // try comment the Arrays.sort(values) or assign other values: Failed assertions should appeaar. 
  
        }
  
      });
  
    }
  
  
  
    public void __init() {
      unsortedArray = (UnsignedInteger[]) UnsignedInteger.createZeroArray(CircuitGenerator.__getActiveCircuitGenerator(), new int[]{SIZE}, 16);
      sortedArray = (UnsignedInteger[]) UnsignedInteger.createZeroArray(CircuitGenerator.__getActiveCircuitGenerator(), new int[]{SIZE}, 16);
    }
  
    private UnsignedInteger[] unsortedArray;
    private UnsignedInteger[] sortedArray;
  
    private static int SIZE = 1024;
    @Override
    public void __defineInputs() {
      super.__defineInputs();
  
  
      unsortedArray = (UnsignedInteger[]) UnsignedInteger.createInputArray(CircuitGenerator.__getActiveCircuitGenerator(), Util.getArrayDimensions(unsortedArray), 16);
  
  
  
  
  
  
  
  
  
    }
    @Override
    public void __defineVerifiedWitnesses() {
      super.__defineVerifiedWitnesses();
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
    }
    @Override
    public void __defineWitnesses() {
      super.__defineWitnesses();
  
  
  
  
      sortedArray = (UnsignedInteger[]) UnsignedInteger.createWitnessArray(CircuitGenerator.__getActiveCircuitGenerator(), Util.getArrayDimensions(sortedArray), 16);
  
  
  
  
  
  
  
  
    }
    @Override
    public void __defineOutputs() {
      super.__defineOutputs();
  
  
  
  
  
  
  
    }
    public void outsource() {
  
      // Use the external code block to compute outside the circuit (More on its usage later in documentation) 
      // The values this block reads from the circuit are the latest values assigned to the variables it relies on,  
      // therefore, care is sometimes needed. The following case is simple though. 
      CircuitGenerator.__getActiveCircuitGenerator().__specifyProverWitnessComputation(new Instruction() {
        public void evaluate(CircuitEvaluator p0) {
  
          BigInteger[] values = new BigInteger[SIZE];
          // read the value from the circuit 
          for (int i = 0; i < SIZE; i++) {
            values[i] = unsortedArray[i].getValueFromEvaluator(CircuitGenerator.__getActiveCircuitGenerator().__getCircuitEvaluator());
          }
          // now values is an array of numbers read from the circuit  
  
          // find the permutation that makes the input sorted 
          Integer[] idxs = new Integer[SIZE];
          for (int i = 0; i < SIZE; i++) {
            idxs[i] = i;
          }
          IndexComparator comparator = new IndexComparator(values);
          // use java sorting -- basically we can use external code not compiled in xjsnark 
          // figure out the locations of elements after sorting 
          Arrays.sort(idxs, comparator);
          int[] permutation = new int[SIZE];
          for (int i = 0; i < SIZE; i++) {
            permutation[idxs[i]] = i;
          }
          // now we sort the array itself 
          Arrays.sort(values);
          // assign the sorted values to our witnesses 
          for (int i = 0; i < SIZE; i++) {
            sortedArray[i].mapValue(values[i], CircuitGenerator.__getActiveCircuitGenerator().__getCircuitEvaluator());
          }
  
          // give the permutation hint to circuit during evaluation 
          CircuitGenerator.__getActiveCircuitGenerator().__getCircuitEvaluator().getPermutations().put("ext_" + "p1", permutation);
        }
      });
  
      // The part that is actually in the circuit 
      new PermutationVerifier(unsortedArray, sortedArray, "p1", UnsignedInteger.__getClassRef(), new Object[]{"16"});
  
  
      for (int i = 0; i < SIZE - 1; i++) {
        CircuitGenerator.__getActiveCircuitGenerator().__addOneAssertion(sortedArray[i].isLessThanOrEquals(sortedArray[i + 1]).getWire());
      }
  
    }
  
    public void __generateSampleInput(CircuitEvaluator evaluator) {
      __generateRandomInput(evaluator);
    }
  
  }
  