For example, lets consider 3 IF for secure channel: IF1 will take message m from Alice as input, and outputs m to Eve. IF2 will take message m, and outputs the encryption of m. IF3 will take message m, and outputs nothing but the size of m. Informally, I don't consider IF1 as meaningful (in the context of secure channel) because an eavedropper can learn m, which is not what you expect from a secure channel: I will say that IF1 is not secure (if you prefer, you can replace "secure IF" with "meaningful IF"). IF2 and IF3 are "more meaningful/secure" because a bounded Eve cannot directly learn m.

If we just talk purely mathematically, then yes, UC/CC only defines secure protocols, and the Ideal Functionality (IF) is the definition of security, so there is no notion of secure IF. Now, in practice, one must ask the question "what are the meaningful IF": otherwise, any protocol can be proven UC secure by taking trivial/stupid IF. This question is out of the scope of the CC framework directly, but anyone wanting to understand the UC framework must understand informally what are these meaningful IF. [see next comment...]

@Sebastian Moreover, when I say that an Ideal Functionality is "information theoretically secure", I indeed abuse a bit the word secure, you are right, the security is by definition. I just use that term to clarify that one should not see any encryption/computationally secure notion in the Ideal Functionality (remember that in the original question, the OP wanted to put the AES protocol directly in the ideal functionality).

@Sebastian Yes, this is very true. I though that I mentioned it, but you are right I did not write it explicitly, so I just corrected my post, thanks (see short sentence + large remark at the end). The reason I focus mainly on information theoretically secure Ideal Functionalities is that in practice you want to be able to quantify clearly the security of a given protocol, and basically computationally secure Ideal Functionalities do not bring much benefit over game based security. See my remark in the post for more details.

Ok I see, thanks a lot. Also, note to myself: in LWE we actually obtain (once scaled by $q$) a continuous Gaussian modulo $q$. If we do the same process, except that we replace all vectors by their expression modulo $q$ (including the input of the distribution), it is not hard to show that this process is the same as if we directly take the modulus of the initial distribution. Said differently, we can also round continuous modulus distributions into discrete continuous distributions with the same parameters.

Oh, I realize I've one more question (after I stop bothering you... at least for today). In Theorem 3.1 you also give a conditional distribution version. However, as far as I understand, if you fix $\bar{x}_1$, you are (when $n$ is high), exponentially unlikely to sample $x_1 = \bar{x}_1$ right? So to output one sample, it takes exponential time. And if you don't fix $\bar{x}_1$, I don't see on what you would do the conditioning. So is this part of the theorem only useful to help to write proofs later, or is there any sort of efficient sampling that you can do from it?

I also thought it was that section, but in fact, as Peikert mentionned, the relevant part was in the section 3, special case of Theorem 3.1. Problem solved! Thanks for the help!

Oh indeed, I made a stupid mistake (forgot to put the $s$ when turning $\rho_{1/s}$ into it's definition with $\exp$, and I did not realize that the expression was not making sense). Anyway, it's solved now, I can sleep. Thanks a lot for your help, it was super useful!

Ok, thanks a lot for your confirmation. So when I write $s I \geq \eta_\varepsilon(\mathbb{Z})$, I follow definition 2.3, i.e. $\eta_\varepsilon(s \mathbb{Z}) \leq 1$. When I write $s \geq \eta_\varepsilon(\mathbb{Z})$, I just compare two reals. I was expecting these two concepts to match, but as far as I can see, they don't (notably because I can't prove that $\eta_\varepsilon(\alpha \Lambda) = \alpha \eta_\varepsilon(\Lambda)$). After maybe I missed something obvious, I'm a bit tired and if you tell me they should match I'll check again tomorrow.

My second question is a bit more general: my goal being to reduce it to $GapSVP_\gamma$, is it the tighter way to reduce $GapSVP_\gamma$ to this true discrete Gaussian sampling? (i.e. to go from GapSVP to continuous, then to true discrete with this additional lose)

The first thing I want to check is that if $x_2$ is sampled via $\Sigma_2 = s^2 I$ and if I choose $\Sigma_1 = s_1^2 I$, then my final sample will have covariance $\Sigma = (s^2+s_1^2)I$. Due to the conditions we must have $s_1 \geq \sqrt{\ln(2n(1+1/\varepsilon))/\pi} = \omega(\sqrt{\log n})$ right? (I was thinking at the beginning that if $s I \geq \eta_\varepsilon(\mathbb{Z})$, then $s \geq \eta_\varepsilon(\mathbb{Z})$, but I don't think it's true, so the best upper bound I can obtain is from the lemma 3.3 of [MR04]). Is it the correct additional noise that I am supposed to obtain?

Thank you very much, it was super useful! I was trying to see how the section "Randomized Rounding" could help me, but in fact it was the previous section on convolved discrete Gaussians! So I tried to redo the proof (at least for my use case, which is, for references, the marginal distribution of continuous $x_2$), and everything is much clearer now (in that case we even get a better statistical distance of $2 \varepsilon$ if I understood correctly). However, I still want to double check some things with you (see next comments):

I'm not sure exactly what is the randomized rounding you mention, but it could be exactly what I need (I don't think it's used in Regev05): according to [GMPW20] page 3 "If desired, these [continuous] samples can then be randomly rounded to have discrete Gaussian error [Pei10]". However, I don't understand how/where [Pei10] is useful with that respect.

Well my problem is not with using $\lfloor\mathcal{D}_{\sigma}\rceil$ (that one is secure for me due to the trivial reduction from continuous LWE that is itself a reduction from GapSVP, which is done in the Regev05), but rather I don't see why $\mathcal{D}_{\mathbb{Z},\sigma}$ is as secure as GapSVP. I checked the CLWE, and indeed it's a different version, where the $s$ and $a$ are continuous, which is basically the oppositve quesiton (I ask can we discretize $e$ with true Gaussian).