Naso: Non-aliasing Affine Systems Orchestrator

fn create_bell_pair(inout q0: [1] Qubit, inout q1: [1] Qubit) -> [0] Proof {
  hadamard(inout q0);
  cnot(inout q0, inout q1);
  // q0, q1 now form a Bell pair |00⟩ + |11⟩
  // Automatic uncomputation on scope exit
}

fn matmul(A: [N][M] f64, B: [M][P] f64) -> [N][P] f64 {
  let C = [[0.0; P]; N];
  for i in 0..N {        // [*] outer loop
      for j in 0..P {    // [*] outer loop
          for k in 0..M { // [M] bounded by polyhedral domain
              C[i][j] += A[i][k] * B[k][j];
          }
      }
  }
  C
}

fn safe_get(arr: [*] [N] f64, idx: usize) -> f64 {
  let mut solver = new_solver();
  let idx_e = expr_from(idx);
  let n_e = expr_from(N);
  
  // Prove 0 <= idx < N at compile time
  assert(&mut solver, idx_e >= expr_from(0));
  assert(&mut solver, idx_e < n_e);
  
  match check(&solver) {
      CheckResult::Sat => arr[idx],           // Bounds proven — no runtime check
      CheckResult::Unsat => compile_error!("Index out of bounds"),
      CheckResult::Unknown => if idx < N { arr[idx] } else { panic!() }
  }
}