Non-interactive proof of value in MPC Does it exist? Specifically using Shamir secret sharing based MPC and looking for a (non-)interactive way to prove that the secret value is valid. A value is valid if it is part of a set for example $[0,1] \in \mathbb Z $ or non-negative, or at least that it is the secret key of some other value. For example if $s$ is the secret and $h=a^s \bmod p$ is the encrypted message and I distribute $s$ using secret sharing, can I prove to the receivers that the shared value is indeed the $s$ value used in $h$?
Here is the simpler method I can think of: let's assume some PKI has been setup, so that there is a known public key $\mathsf{pk}_i$ for each receiver $R_i$. Then, the share sender can simply broadcast a list $c_i = \mathsf{Enc}_{\mathsf{pk}_i}(s_i)$ to everyone, where $\mathsf{Enc}$ is some encryption scheme and the $s_i$ form the secret shares of the secret $s$. This allows each receiver $R_i$ to retrieve his share (and only his share), but also adds a public value that binds the share sender to each share - this is necessary if you want to prove anything.

Then, the share sender can use any standard NIZK proof system to prove the following NP statement:
$\{\exists (r_1, s_1, \cdots, r_n, s_n): \forall i\leq n, c_i = \mathsf{Enc}_{\mathsf{pk}_i}(s_i;r_i)  \wedge F(\mathsf{Reconstruct}(s_1, \cdots, s_n)) = 1\}$,

where $\mathsf{Reconstruct}$ is the reconstruction algorithm of the sharing scheme you are using, and $F$ is the function that checks whatever you want to check about the secret $s$ (e.g. $F$ could return 1 if and only if its input is a bit, if you want to check that $s\in \{0,1\}$).

Depending on the encryption scheme used, the secret sharing scheme used, and the function $F$, the NIZK will be more or less complex - but it is always theoretically feasible to build such a proof (under a variety of standard cryptographic assumptions) since it is an NP statement, and we have NIZK proofs for any NP statement.

If you want the NIZK to be efficient, you'll need to use algebraic and compatible schemes - typically, something like the additive variant of ElGamal for the encryption scheme, with a group of prime order $p$, and a secret sharing over $\mathbb{F}_p$. For example, proving that $n$ ElGamal ciphertexts encrypt additive shares (modulo $p$) of a bit can be done relatively efficiently with existing techniques for NIZKs (it's a relatively simple extension of a Schnorr Sigma protocol, plus the usual Fiat-Shamir heuristic - or a Groth-Sahai proof in case you don't want to rely on heuristics).