Quantum search differs from the standard boolean SAT as it is restricted to only oracle calls to a circuit (or CNF formula). Where SAT gives us the structure of a formula (however loosely defined that is), quantum search algorithms make queries to $U_f$.
It seems pretty clear that this oracle-only SAT problem is NP-hard. Of course, it isn't a decision problem, but rather it is an oracle problem, so my notion of reduction is $A \leq B \iff$ "an oracle to solve B can be used to solve A in polytime." (A Turing reduction).
If we had an oracle that solved quantum search, then we could just use this oracle to solve SAT.
But I'm curious on what is known about the inverse; i.e., if we had an oracle that solved SAT, could we solve quantum search? Has it been shown that this isn't true? Intuitively, this being true feels like it proves $P = NP$, but I'm not quite sure.
Also, it's pretty easy to see how quantum search can be verified in polynomial (constant) time. But I am asking if it can reduce to SAT, which is my definition of NP here.