Léo Robert
email: leo.robert@uca.fr

Daiki Miyahara
email: miyahara@uec.ac.jp

Pascal Lafourcade
email: pascal.lafourcade@uca.fr

Takaaki Mizuki
email: mizukilncs@tohoku.ac.jp

Takaaki

Card-Based ZKP Protocol for Nurimisaki

Keywords: Zero-knowledge proof, Pencil Puzzle, Card-based cryptography, Nurimisaki

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The democratization of computers and network systems has fuelled the virtualization of interactions and processes such as communication, pay-ments, and elections. Proving the knowledge of some secret without revealing any bit of information from that secret is crucial in our today's society. This issue can be applied to numerous contexts.

For instance, a client would like to connect to a server via a password without revealing the password. Another example is database management, where an entity could ask if a piece of information is in a database without asking for factual data. A third example can be given in the electronic voting system where the voters want to be sure that the ballots are correctly mixed (without revealing how the mix was done).

A cryptographic tool exists for all the previous examples, called a Zero-Knowledge Proof (ZKP) protocol. It enables a prover P to convince a verifier V that P knows a secret s without revealing anything other than it. A ZKP protocol must verify the following three properties:

-Completeness: If P knows s then the protocol ends without aborting (meaning that V is convinced that P has s); -Soundness: If P does not have s then V will detect it; -Zero-Knowledge: V learns nothing about s.

In practice, ZKP protocols are typically executed by computers. However, their understanding is difficult for the uninitiated. We take a more direct approach to the notion of ZKP and construct a protocol using physical objects like playing cards and envelopes. It allows us to present the notion of ZKP protocols without deep mathematical backgrounds and also to extend the existing literature.

The first physical ZKP protocol [START_REF] Gradwohl | Cryptographic and physical zero-knowledge proof systems for solutions of Sudoku puzzles[END_REF] for a Sudoku grid was constructed using a deck of cards. Since this novel protocol was devised, several teams in the world have proposed physical ZKP protocols using a deck of cards for pencil puzzles, such as Sudoku [START_REF] Ruangwises | Two standard decks of playing cards are sufficient for a ZKP for Sudoku[END_REF][START_REF] Sasaki | Efficient card-based zeroknowledge proof for Sudoku[END_REF], Akari [START_REF] Bultel | Physical zero-knowledge proofs for Akari, Takuzu, Kakuro and KenKen[END_REF], Takuzu [START_REF] Bultel | Physical zero-knowledge proofs for Akari, Takuzu, Kakuro and KenKen[END_REF], Kakuro [START_REF] Bultel | Physical zero-knowledge proofs for Akari, Takuzu, Kakuro and KenKen[END_REF][START_REF] Miyahara | Card-based physical zeroknowledge proof for Kakuro[END_REF], KenKen [START_REF] Bultel | Physical zero-knowledge proofs for Akari, Takuzu, Kakuro and KenKen[END_REF], Makaro [START_REF] Bultel | Physical zero-knowledge proof for Makaro[END_REF], Norinori [START_REF] Dumas | Interactive physical zero-knowledge proof for Norinori[END_REF], Slitherlink [START_REF] Lafourcade | How to construct physical zero-knowledge proofs for puzzles with a "single loop" condition[END_REF], Suguru [START_REF] Robert | Physical zero-knowledge proof and np-completeness proof of suguru puzzle[END_REF], Nurikabe [START_REF] Robert | Card-based ZKP for connectivity: Applications to Nurikabe, Hitori, and Heyawake[END_REF], Ripple Effect [START_REF] Ruangwises | Securely computing the n-variable equality function with 2n cards[END_REF], Numberlink [START_REF] Ruangwises | Physical zero-knowledge proof for Numberlink puzzle and k vertex-disjoint paths problem[END_REF], Bridges [START_REF] Ruangwises | Physical ZKP for connected spanning subgraph: Applications to Bridges puzzle and other problems[END_REF], Cryptarithmetic [START_REF] Isuzugawa | Zero-knowledge proof protocol for Cryptarithmetic using dihedral cards[END_REF], Shikaku [START_REF] Ruangwises | How to physically verify a rectangle in a grid: A physical ZKP for Shikaku[END_REF], and Nonogram [START_REF] Chien | Cryptographic and physical zero-knowledge proof: From Sudoku to Nonogram[END_REF][START_REF] Ruangwises | An improved physical ZKP for Nonogram[END_REF].

Why shall we propose a new card-based ZKP protocol for another Nikoli puzzle? For us, it is similar to the question: Why shall we prove that a puzzle is NP-complete? People want to know if a puzzle is NP-complete in order to know if the puzzle is difficult or not for a computer to solve it. Card-based ZKP protocols are quite similar; once a puzzle is shown to be NP-complete, a natural question is: Can we design a physical ZKP protocol? This is an intellectual challenge on the puzzle. Moreover, each puzzle has different rules and specificity, which force us to imagine new physical ZKP techniques. For instance, consider a Nikoli puzzle, Nurimisaki, which we will deal with in this paper; then, its rules combine for the first time some connectivity, neighbourhood restriction, and straight line with counting, as seen later. A previous work [START_REF] Saito | Physical zero-knowledge proof for the pencil puzzle Nurimisaki[END_REF] (in Japanese, unpublished) proposed a card-based ZKP protocol for Nurimisaki. Yet, the protocol is not optimal since it prepares another grid to verify the rules (so the number of cards is large). Moreover, elaborate but complex techniques are used (e.g., using another grid to represent the in-spanning-tree of P 's solution). In contrast, our protocol has a more direct approach with closer interaction to the real game. Before giving our contributions, let us define the rules of the Nurimisaki puzzle.

Nurimisaki Rules. Figure 1 shows a puzzle instance of Nurimisaki. The goal for Nurimisaki puzzle is to color in black some cells on the grid, under the following rules:

1. A cell with a circle is called a "Misaki". A Misaki has only one cell of its neighbours (vertically or horizontally) remaining white and the rest black. 2. The number written in a Misaki cell indicates the number of white cells in straight line from the Misaki. If there is no number, any number of white cells is allowed. 3. White cells without a circle cannot be a Misaki. 4. A 2 × 2 square cannot be composed of only black or white cells. 5. White cells are connected.

Nurimisaki puzzle was recently proven NP-complete in [START_REF] Iwamoto | Computational complexity of Nurimisaki and Sashigane[END_REF]; hence, it is a natural question to construct a physical ZKP protocol for this fun puzzle. Although Goldwasser et al. [START_REF] Goldwasser | The knowledge complexity of interactive proof-systems[END_REF] proved that any NP-complete problem has its corresponding interactive ZKP protocol, simple physical ZKP protocols are always sollicited as mentioned above.

Contributions. We propose a physical ZKP protocol that only uses cards and envelopes. We rely on some classical existing card-based sub-protocols in order to be able to construct our ZKP protocol. The main difficulty in this Nurimisaki game that seems to be simple, is that existing techniques proposed in the literature since few years cannot be applied directly. The main trick is to find an encoding that allows us to apply several subprotocols in the right order to obtain a secure ZKP protocol. For this, we propose an original way to combine several techniques to design our ZKP protocol with a reasonable amount of cards and manipulations.

Outline. In Section 2, we introduce our encoding scheme using cards in order to represent a gird of the game and a solution. We also give some sub-protocols that are used in our construction. In Section 3, we give our ZKP protocol for Nurimisaki. Before concluding in the last section, we give the security proof of our ZKP protocol in Section 4.

Preliminaries

We explain the notations and sub-protocols used in our constructions.

Cards and Encoding. The cards we use in our protocols consist of clubs

♣ ♣ • • • , hearts ♡ ♡ • • • ,
and numbered cards 1 2 • • • , whose backs are identical ? . We encode three colors {black, white, red} with the order of two cards as follows:

♣ ♡ → black, ♡ ♣ → white, ♡ ♡ → red. (1)
We call a pair of face-down cards ? ? corresponding to a color according to the above encoding rule a commitment to the respective color. We also use the terms, a black commitment, a white commitment, and a red commitment. We sometimes regard black and white commitments as bit values, based on the following encoding scheme:

♣ ♡ → 0, ♡ ♣ → 1. (2)
For a bit x ∈ {0, 1}, if a pair of face-down cards satisfies the encoding (2), we say that it is a commitment to x, denoted by ? ?

x .

We also define two other encoding [START_REF] Ruangwises | Securely computing the n-variable equality function with 2n cards[END_REF][START_REF] Shinagawa | Card-based protocols using regular polygon cards[END_REF]:

-♣-scheme: for x ∈ Z/pZ, there are p cards composed of p -1 ♡s and one ♣, where the ♣ is located at position (x + 1) from the left. For example, 2 in Z/4Z is represented as ♡ ♡ ♣ ♡ . -♡-scheme: it is the same encoding as above but the ♡ and ♣ are reversed. For instance, 2 in Z/4Z is represented as ♣ ♣ ♡ ♣ . where s is uniformly and randomly chosen from Z/mZ. Implementing a pile-shifting shuffle is simple: we use physical cases that can store a pile of cards, such as boxes and envelopes; a player (or players) cyclically shuffles them manually until everyone (i.e., the prover P and the verifier V ) loses track of the offset.

Pile

Input-preserving Five-card Trick [12]

Given two commitments to a, b ∈ {0, 1} based on the encoding rule (2), this sub-protocol [START_REF] Boer | More efficient match-making and satisfiability: The five card trick[END_REF][START_REF] Miyahara | Card-based ZKP protocols for Takuzu and Juosan[END_REF] reveals only the value of a ∨ b as well as restores commitments to a and b: ? ?

a ? ? b → a ∨ b & ? ? a ? ? b .
The original sub-protocol [START_REF] Boer | More efficient match-making and satisfiability: The five card trick[END_REF][START_REF] Miyahara | Card-based ZKP protocols for Takuzu and Juosan[END_REF] was designed for computing AND (a ∧ b), but we adjust it to compute OR (a ∨ b):

1. Add helping cards and swap the two cards of the commitment to b so that we have the negation b, as follows:

? ? a ? ? b → ? ? a ♡ ? ? b ♡ ♣ ♣ ♣ ♣ .
2. Rearrange the sequence of cards and turn over the face-up cards as:

? ? ♡ ? ? ♡ ♣ ♣ ♣ ♣ → ? ♡ ? ♣ ♡ ♣ ? ♣ ? ♣
→ ? ?

? ?

? ?

? ? ? ?

.

3. Regarding cards in the same column as a pile, apply a pile-shifting shuffle to the sequence:

? ?

? ?

? ?

? ? ? ? → ? ? ? ? ? ? ? ? ? ? .

4. Reveal all the cards in the first row.

(a

) If it is ♣ ♣ ♡ ♡ ♡ (up to cyclic shifts), then a ∨ b = 0. (b) If it is ♡ ♣ ♡ ♣ ♡ (up to cyclic shifts), then a ∨ b = 1.

5.

After turning over all the face-up cards, apply a pile-shifting shuffle.

6. Reveal all the cards in the second row; then, the revealed cards should include exactly one ♡ . 7. Shift the sequence of piles so that the revealed ♡ is the leftmost card and swap the two cards of the commitment to b to restore commitments to a and b.

Mizuki-Sone Copy Protocol [14]

Given a commitment to a ∈ {0, 1} along with four cards ♣ ♡ ♣ ♡ , the Mizuki-Sone copy protocol [START_REF] Mizuki | Six-card secure AND and four-card secure XOR[END_REF] outputs two commitments to a:

? ? a ♣ ♡ ♣ ♡ → ? ? a ? ? a .
1. Turn all cards face-down and set the commitments as follows:

? ?

How to Form a White Polyomino [17]

We introduce the generic method of [START_REF] Robert | Card-based ZKP for connectivity: Applications to Nurikabe, Hitori, and Heyawake[END_REF] to address the connectivity constraint (rule 5). Given a grid where all cells are black, it enables P to make white connected cells, i.e., white-polyomino, without revealing anything to V . We first describe two crucial sub-protocols: the chosen pile protocol and the 4-neighbor protocol.

Chosen pile protocol [START_REF] Dumas | Interactive physical zero-knowledge proof for Norinori[END_REF]. The chosen pile protocol allows P to choose a pile of cards without V knowing which one. This pile can be manipulated and all the commitments are replaced to their initial order afterward. This protocol is an extended version of the "chosen pile cut" proposed in [START_REF] Koch | Foundations for actively secure card-based cryptography[END_REF]. Given m piles (p 1 , p 2 , . . . , p m ) with 2m additional cards, the chosen pile protocol enables a prover P to choose the i-th pile p i (without revealing the index i) and revert the sequence of m piles to their original order after applying other operations to p i . 2. Considering the cards in the same column as a pile, apply a pileshifting shuffle to the sequence of piles. 3. Reveal all the cards in row 2. Then, exactly one ♡ appears, and the pile above the revealed ♡ is the i-th pile (and hence, P can obtain p i ). After this step is invoked, other operations are applied to the chosen pile. Then, the chosen pile is placed back to the i-th position in the sequence. 4. Remove the revealed cards, i.e., the cards in row 2. (Note, therefore, that we do not use the card ♡ revealed in Step 3.) Then, apply a pile-shifting shuffle. 5. Reveal all the cards in row 3. Then, one ♡ appears, and the pile above the revealed ♡ is p 1 . Therefore, by shifting the sequence of piles (such that p 1 becomes the leftmost pile in the sequence), we can obtain a sequence of piles whose order is the same as the original one without revealing any information about the order of the input sequence.

Sub-protocol: 4-Neighbor Protocol [START_REF] Robert | Card-based ZKP for connectivity: Applications to Nurikabe, Hitori, and Heyawake[END_REF]. Given pq commitments placed on a p × q grid, a prover P has a commitment in mind, which we call a target commitment. The prover P wants to reveal the target commitment and another one that lies next to the target commitment (without revealing their exact positions). Here, a verifier V should be convinced that the second commitment is a neighbor of the first one (without knowing which one) as well as V should be able to confirm the colors of both the commitments. To handle the case where the target commitment is at the edge of the grid, we place commitments to red (as "dummy" commitments) in the left of the first column and below the last row to prevent P from choosing a commitment that is not a neighbor. Thus, the size of the expanded grid is (p + 1) × (q + 1). This sub-protocol proceeds as follows.

1. P and V pick the (p + 1)(q + 1) commitments on the grid from left-to-right and top-to-bottom to make a sequence of commitments: ? ? ? ? ? ? ? ? • • • ? ? . 2. P uses the chosen pile protocol to reveal the target commitment. 3. P and V pick all the four neighbors of the target commitment. Since a pile-shifting shuffle is a cyclic reordering, the distance between commitments are kept (up to a given modulo). That is, for a target commitment (not at any the edge), the possible four neighbors are at distance one for the left or right one, and p + 1 for the bottom or top one so that P and V can determine the positions of all the four neighbors. 4. Among these four neighbors, P chooses one commitment using the chosen pile protocol and reveals it. 5. P and V end the second and first chosen pile protocols.

Forming white-polyomino. Assume that there is a grid having p × q cells. P wants to arrange white commitments on the grid such that they form a white-polyomino while V is convinced that the placement of commitments is surely a white-polyomino. The sub-protocol proceeds as follows.

1. P and V place a commitment to black (i.e., ♣ ♡ ) on every cell and commitments to red as mentioned above so that they have (p+1)(q+1) commitments on the board. 2. P uses the chosen pile protocol to choose one black commitment that P wants to change.

(a) V swaps the two cards constituting the chosen commitment so that it becomes a white commitment (recall the encoding (1)). (b) P and V end the chosen pile protocol to return the commitments to their original positions. 3. P and V repeat the following steps exactly pq -1 times.

(a) P chooses one white commitment as a target and one black commitment among its neighbors using the 4-neighbor protocol; the neighbor is chosen such that P wants to make it white. (b) V reveals the target commitment. If it corresponds to white, then V continues; otherwise V aborts.

(c) V reveals the neighbor commitment (chosen by P ). If it corresponds to black, then P makes the neighbor white or keep it black (depending on P 's choice) by executing the following steps; otherwise V aborts. ii. Regarding cards in the same column as a pile, V applies a pileshifting shuffle to the sequence of piles: ? ? ? ? → ? ? ? ? . iii. V reveals the two cards in the second row. If the revealed right card is ♡ , then V swaps the two cards in the first row; otherwise V does nothing.

(d) P and V end the 4-neighbor protocol.

V is now convinced that all the white commitments represent a whitepolyomino. Therefore, this method allows a prover P to make a solution that only P has in mind, guaranteed to satisfy the connectivity constraint.

Sum in Z [22]

We give a brief overview (formally defined in Appendix A) of the protocol described in [START_REF] Ruangwises | Securely computing the n-variable equality function with 2n cards[END_REF] for the addition of elements in Z/2Z with a result in Z. This allows to compute S = n i=1 x i with S ∈ Z and x i ∈ Z/2Z for i ∈ {1, . . . , n}. The idea is to compute the sum inductively; when starting by the two first elements x 1 and x 2 , they are transformed into x 1 -r and x 2 + r for uniformly random r ∈ Z/2Z. Then x 2 + r is revealed (no information about x 2 leaks since r is random), and the cards of x 1 -r is shifted by x 2 + r positions to encode value (x 1 -r) + (x 2 + r) = x 1 + x 2 . Note that this result is in Z/(p + 1)Z (or simply Z since the result is less than p) for elements x 1 , x 2 in Z/pZ.

Setup phase

The verifier V and the prover P place black commitments on all the cell of the p × q grid and place red commitments ("dummy" commitments) around the grid so that we have (p + 1)(q + 1) commitments.

Connectivity phase

P and V apply the protocol given in Section 2.4: a white-polyomino is formed according to P 's solution. Now, V reveals all the commitments corresponding to Misaki to check that they are indeed white. After this phase, V is convinced that white commitments are connected (rule 5).

Verification Phase

The verifier V is now checking that the other rules are satisfied.

No 2 × 2 square (rule 4). We use an adapted verification phase of the one in [START_REF] Robert | Card-based ZKP for connectivity: Applications to Nurikabe, Hitori, and Heyawake[END_REF] for checking that 2 × 2 square are not composed of only white (black) commitments. Note that for an initial grid p × q, there are (p -1)(q -1) possible squares of size 2 × 2. Thus P and V consider each of those squares (in any order) and apply the following:

1. P chooses a white commitment and a black one among the four commitments via the chosen-pile protocol (Section 2.4). 2. V reveals both commitments marked by P in the previous step. If there are exactly a white commitment and a black one, V continues; otherwise, abort.

Misaki (rule 1 and 2). V wants to check that each Misaki cell (cell with a circle) has only one of its neighbours white and others black. Moreover, when a Misaki has a number in it, V wants to check that the straight line formed by white cells starting from the Misaki cell has the corresponding number of white cells. P and V first consider Misaki cells with a number. For each Misaki cell (not at a border) with a number i in it, apply the following:

1. P and V add black commitments (i.e., "dummy" commitments) at the border of the grid. This ensures that we delimit correctly the number of white commitments in straight line. 2. For each of the four neighbours, P and V form a pile composed of i + 1 commitments for each direction (top, bottom, left, right). If there is exactly one commitment corresponding to white then V continues. Otherwise, V aborts. 5. V reveals the next i commitments of the pile with the first white commitment. If there are only white commitments for the first i -1 commitments and a black commitment for the last one, then V continues; otherwise, aborts.

After this step, V is convinced that Misaki cells with a number are well-formed. In the case where there is no number, the first step consists of forming a pile with only one commitment. Hence, V is convinced that Misaki cells without a number satisfy only rule 1 but not rule 2 since any number of white cells could form the straight line.

Note that we described the protocol for Misaki cell not at the border of the grid. If a Misaki cell is at a border (but not a corner) then the 4neighbours becomes the 3-neighbours and the protocol is the same (there will be only three piles instead of four). For Misaki cells at a corner, P and V consider the 2-neighbours (thus only two piles).

No circle, no Misaki (rule 3). V needs to check that white cells without a circle are not Misaki, meaning that any white cell of the grid has at least two of its neighbours white. This rule is somewhat challenging to verify without leaking information on the solution because the number and location of white cells are part of the solution (and must not be publicly revealed).

If the targeted cell is black then there is nothing to verify since any configurations could occur. Yet, if the targeted cell is white then there are at least (but it could be more) two neighbours that are white. The idea is to set the value of targeted cell being 5 if it is white and 0 if it is black. Then we add the neighbours to it (white is 0, and black is 1). If the cell is black then the sum is always less than or equal to 4 (which is permitted by the rules to have all black). But if the cell is white then the permitted value for the sum is less than or equal to 7 (a Misaki is equal to 8) for a targeted cell that is not at a border.

For a given cell, called targeted cell c t , we look at its neighbors (up to 4). The idea of verifying that a white cell is not a Misaki is to first sum the four neighbors (where a white cell is equal to 0 and a black cell is 1). Then by choosing another encoding, the targeted cell can be equal to 5 for white and 0 for black. Finally, adding the sum of the neighbors with c t gives at most 4 for black c t (which is permitted by the rules) and at most 7 for white c t in a valid configuration and 8 or 9 for invalid configuration.

1. Copy all the commitments using the copy protocol (Section 2.3). The number of copies for a p × q grid is 2(2pq -p -q); we leave the detailed computations in Appendix B. 2. Sum the four neighbours by considering that a white commitment is equal to 0 and a black commitment is equal to 1. The result is given in ♡-scheme (i.e., there are four ♣ s and one ♡ at position corresponding to the result of the sum). 3. For the targeted cell, add 3 ♡ in the middle of the commitment as:

white: ♡ ♣ → ♡ ♡ ♡ ♡ ♣ = 5, black: ♣ ♡ → ♣ ♡ ♡ ♡ ♡ = 0.
White is now 5 and black is 0 in the ♣-scheme. 4. Sum the result of the two previous steps (the sum of the four neighbours and the inner cell). The result is encoded in the ♡-scheme. 5. Reveal the last and penultimate cards. If a ♡ appears then abort; otherwise, continue.

Security Proofs

Our protocol needs to verify three security properties given as theorems.

Theorem 1 (Completeness). If P knows the solution of a Nurimisaki grid, then P can convince V .

Proof. First, notice that P convinces V in the sense that the protocol does not abort which mean that all the rules are satisfied. The protocol can be split in two: (1) the connectivity and (2) the verification phases.

(1) Since P knows the solution, the white cells are connected and hence can always choose a black commitment at step 2 to swap it to white. Notice that there exists a proof for the connectivity in [START_REF] Robert | Card-based ZKP for connectivity: Applications to Nurikabe, Hitori, and Heyawake[END_REF].

(2) The verification of 2 × 2 square will not abort since if P has the solution then for any given 2 × 2 square there always exist a white commitment and a black commitment. For the Misaki rules, each Misaki cell has three of its neighbors black and one white; thus, the first commitment of piles p 1 , p 2 , p 3 , p 4 will reveal exactly three black and one white commitments. Then, when looking at pile p i of the first commitment corresponding to white, the number of white commitments corresponds to the number in the inner cell. Thus the protocol will continue. Finally, the non-Misaki rule is verified. Since P has the solution, any white cell (with no circle in it) has at least two white neighbors. Thus if the inner cell is white then the sum will start to 5 and the maximal value is 7 because a solution has at least two whites so at most two black commitments (of value 1 in this step). So the protocol will continue and hence V will be convinced that P has the solution.

Theorem 2 (Soundness). If P does not provide a solution of the p × q Nurimisaki grid, P is not able to convince V .

Proof. Suppose that P does not know the solution, hence at least one of the rules is not verified. If the white cells are not connected then P cannot choose a black commitment at step 2 hence V will detect it. Notice that there is also the proof of this phase in [START_REF] Robert | Card-based ZKP for connectivity: Applications to Nurikabe, Hitori, and Heyawake[END_REF].

If P does not have the solution, then one of the verification phase will fail. We apply a case distinction for those verifications. Assume first that there is a block of 2 × 2 square composed of only white (black) commitments, then P cannot choose, during the chosen-pile protocol, two distinct commitments (i.e., a black and a white) thus the revealed commitments will attest to V that P does not have the solution. Second, assume that a Misaki cell is not well-formed in the sense that either (1) the number of white neighbour is not equal to 1 or that (2) the number of white cells in straight line does not correspond to the number of the Misaki cell. For (1) the neighbours are revealed (after a shuffle) so V will notice the number of white commitments; for (2) all the commitments next to the white neighbour are revealed thus V will also notice if there is a flaw. The last verification is for white cells which are not Misaki. It is equivalent of saying that any white cell (without a circle in it) has at least two white neighbours. If a white cell has only one white neighbour then during the sum process, then c t = 5 (because the central cell is white) and the total for its neighbours is 3 (because there are 3 black commitments and 1 white). The final sum is then equal to 8, since V will look at the last and penultimate card of the sum (corresponding to a sum equal to 9 and 8) then V will detect that a white card is a Misaki. Notice that a sum equals to 9 means the white cell is surrounded by 4 black cells. It is not possible since white cells are connected.

Theorem 3 (Zero-knowledge). V learns nothing about P 's solution of the given grid G.

Proof. We use the same proof technique as in [START_REF] Gradwohl | Cryptographic and physical zero-knowledge proof systems for solutions of Sudoku puzzles[END_REF], namely the description of an efficient simulator which simulates the interaction between an honest prover and a cheating verifier. The goal is to produce an indistinguishable interaction from the verifier's view (with the prover). Notice that the simulator does not have the solution but it can swap cards during shuffles. Informally, the verifier cannot distinguish between two protocols, one that is run with the actual solution and one with random commitments. The simulator acts as follows: The simulator constructs a random connected white polyomino. During the 2 × 2 square verification, the simulator will swap cards to choose white and black commitments. For the Misaki verification, the simulator swaps three commitments to black for three piles and one to white for the last pile. The latter will also be modified by the simulator to contain the correct numbers of white commitments (and the last commitment to black). During the non-Misaki verification, when the sum is computed, the simulator swaps the cards to always put ♣ cards in position 8 and 9 (for the cell not at the edge, but the latter is done the same way).

The simulated and real proofs are indistinguishable hence V learns nothing from the connectivity and verification phases. Finally, we conclude that the protocol is zero-knowledge.

Conclusion

We proposed a physical ZKP protocol for Nurimisaki that uses only cards and envelopes. The most difficult part was to prove that cells are not Misaki without leaking their color. Of course, we combined this part with the rest of the verifications that are stated by other rules. This new approach clearly demonstrates that showing that some cells do not have some properties is often more difficult than proving an explicit property without leaking any information. The next step is to see if this new trick can be applied for other Nikoli's games. For instance, Moon-or-Sun is one possible candidate. Going further the puzzle Shakashaka is even more challenging since it combines such tricks with geometrical shapes, which is more difficult. or 1): ? ?

x 1 ? ?

x 2 ♣ ♡ → ? ? ?

x 1 +x 2 .

1. Swap the two cards of the commitment to x 1 and add a ♣ face down to the right. Those three cards represent x 1 in the ♡-scheme in Z/3Z.

-→ ←-? ?

x 1 ? ♣ → ? ? ?

x 1 .

2. Add a ♡ on the right of the commitment to x 2 . Those three cards represent x 2 in the ♣-scheme in Z/3Z.

? ?

x 2 ? ♡ → ? ? ?

x 2 .

3. Obtain three cards representing x 1 + r and those representing x 2 -r for a uniformly random value r ∈ Z/3Z as follows.

(a) Place in reverse order the three cards obtained in Step 2 below the three cards obtained in Step 1:

? ? ?

x 1 ? ? ?

x 2 → ? ? ?

x 1 ? ? ? .

For a uniformly random value r ∈ Z/3Z, we obtain three cards representing x 1 + r and those representing 2 -x 2 + r. (c) Rearrange the three cards representing 2 -x 2 + r to obtain those representing x 2 -r:

? ? ?

x 1 +r ? ? ?

x 2 -r .

4. Reveal the three cards representing x 2 -r, and shift to the right the three cards representing x 1 + r to obtain those representing x 1 + x 2 in the ♡-scheme; apply the same routine for the remaining elements to compute the final sum.

Notice that we described the protocol for a result in Z/3Z but it is easily adaptable for a result in, let say, Z/qZ. Indeed, during the first step, we add a single ♣ to the first commitment and a single ♡ to the second; thus for a sum that could be equal to q -1, we add q -2 ♣ s to the first commitment and q -2 ♡ s to the second.

B Number of copies

The number of calls to copy protocol can be expressed given the size of the grid p × q. Indeed, we can split the cells in three categories: (1) cells at a corner, (2) cells at a border but not at a corner and (3) cells at the middle of the grid. First, notice that the copy protocol is called for the same number of neighbors the cell has. Thus, the copy protocol is run, given each type of cell: corner: 2, border: 3, middle: 4. Thus, by computing the total number of cells for each type, we can find the total number of calls to the copy protocol. The number of cell for each category, for a p × q grid, is: corner: 4, border: 2(p -2) + 2(q -2) = 2(p + q -4), middle: (p -2)(q -2).

Finally, the total number of calls to the copy protocol N c is:

N c = 2 × 4 + 3 × 2(p + q -4) + 4 × (p -2)(q -2) = 8 + 6p + 6q -24 + 4pq -8p -8q + 16 = 2(2pq -p -q).

Fig. 1 .

 1 Fig. 1. Nurimisaki example (left) with its solution (right).

  i. If P wants to change the commitment, P places face-down club-to-heart pair below it; otherwise, P places a heart-to-club pair: ? ? → ? ?

4 3.p 2 p 3 p 4 1 2 3 4 4 .

 444 P and V puts numbered cards under each pile as follows: p 1 P and V shuffle the piles and reveal the first commitment of each pile.

-shifting Shuffle [15, 26]

	This shuffling action means to cyclically shuffle piles of cards. More for-
	mally, given m piles, each of which consists of the same number of face-
	down cards, denoted by (p 1 , p 2 , . . . , p m ), applying a pile-shifting shuffle
	(denoted by ⟨•∥ • • • ∥•⟩) results in (p s+1 , p s+2 , . . . , p s+m ):
	? p 1	? p 2	• • •	? p m	→	? p s+1 p s+2 ? • • • ? p s+m	,

  1. Using m -1 ♣ s and one ♡ , P places m face-down cards encoding i -1 in the ♡-scheme (denoted by row 2) below the given piles, i.e., only the i-th card is ♡ . We further put m cards encoding 0 in the ♡-scheme (denoted by row 3): ?

		?	. . . ?	?	?	. . . ?
	p 1	p 2	p i-1	p i	p i+1	p m
	?

♣ ? ♣ . . . ? ♣ ? ♡ ? ♣ . . . ? ♣ ← row 2 ? ♡ ? ♣ . . . ? ♣ ? ♣ ? ♣ . . . ? ♣ ← row 3

⋆ We thank the anonymous referees, whose comments have helped us to improve the presentation of the paper. This work was supported in part by JSPS KAKENHI Grant Number JP19J21153. This study was partially supported by the French ANR project ANR-18-CE39-0019 (MobiS5).

ZKP Protocol for NurimisakiWe present our ZKP protocol for Nurimisaki. Hereinafter, we consider an instance of Nurimisaki as a rectangular grid of size p × q.

A Sum of commitments

We describe the protocol in [START_REF] Ruangwises | Securely computing the n-variable equality function with 2n cards[END_REF] for adding elements in Z/2Z with a result in Z.

Given commitments x i ∈ Z/2Z for i ∈ {1, . . . , n} along with one ♣ and ♡ , the protocol produces their sum S = n i=1 x i in Z/(n + 1)Z encoded in the ♡-scheme without revealing the values of x i . The idea is to compute the sum inductively; when starting by the two first commitments to x 1 and x 2 , they are transformed into x 1 -r and x 2 + r encoded in the ♡-scheme and ♣-scheme, respectively, for uniformly random value r ∈ Z/3Z. Then x 2 + r is revealed (no information about x 2 is revealed because r is random), and x 1 -r is shifted by x 2 + r positions to encode

Note that this result is in Z/(p + 1)Z (or simply Z because the result is less than or equal to p) for elements x 1 , x 2 in Z/pZ.

The protocol is now formally described. First notice that a black cell is assumed to be equal to 1 and a white cell is equal to 0 (according to Eqs. (1) and ( 2)). Consider first two commitments to x 1 and x 2 (either 0


Gaëtan Gilbert

Yann Leray

Nicolas Tabareau

Théo Winterhalter

The Rewster: The Coq Proof Assistant with Rewrite Rules

Dependently typed languages such as Coq or Agda are very convenient tools to program with strong invariants and develop mathematical proofs. However, a user might be inconvenienced by things such as the fact that n and n+0 are not considered definitionally equal, or the inability to postulate one's own constructs with computation rules such as exceptions [START_REF] Pédrot | Failure is Not an Option An Exceptional Type Theory[END_REF]. Coq modulo theory [START_REF] Strub | Coq modulo theory[END_REF] solves the first of the two problems by extending Coq's conversion with decision procedures, e.g., for linear integer arithmetic. Rewrite rules can be used to deal with directed equalities for natural numbers, but also to implement exceptions that compute. They were introduced in Agda [CA16] a few years ago, and later extended to provide more guarantees with a modular confluence checker [START_REF] Cockx | How to tame your rewrite rules[END_REF][START_REF] Cockx | The Taming of the Rew: A Type Theory with Computational Assumptions[END_REF].

We present a work-in-progress extension1 of Coq which supports user-defined rewrite rules. While we mostly follow in the footsteps of the Agda implementation, we also have to face new issues due to the differences in the implementation and meta-theory of Coq and Agda. The most prominent one being the different treatment of universes as Coq supports cumulativity but no first-class universe levels. We will take advantage of this talk to expose our ideas on how to solve the different issues that arise when adding user-defined rewrite rules to a proof assistant by integrating2 rewrite rules in MetaCoq [SAB + 20, SBF + 20], building on previous work [START_REF] Cockx | How to tame your rewrite rules[END_REF][START_REF] Cockx | The Taming of the Rew: A Type Theory with Computational Assumptions[END_REF].

Rewrite Rules in Coq. We only support rewrite rules whose head symbol is declared as such with the Symbol command, which essentially declares an axiom for which we can postulate computation rules. Rules are then declared using the Rewrite Rule command. For instance:

Symbol pplus : N → N → N. Rewrite Rule [ n ] ⊢ pplus 0 n =⇒ n. Rewrite Rule [ n ] ⊢ pplus n 0 =⇒ n. Rewrite Rule [ n m ] ⊢ pplus (S n) m =⇒ S (pplus n m). Rewrite Rule [ n m ] ⊢ pplus n (S m) =⇒ S (pplus n m).
will declare the parallel plus that computes on both its arguments. On the left of the turnstile (⊢) variables are quantified and can furthermore be annotated with their type. We will illustrate the features and specificities of our implementation below, while exposing the challenges that come with them.

Non-Linearity. For now, we restrict our rewrite rules to be left-linear: each variable can only appear once on the left-hand side of the rule. This appears like a very strong limitation as certain rules are only well typed in presence of non-linearity: e.g., the computation rule for the J eliminator. This can be circumvented by forcing certain variables to be equal to an expression:

Rewrite Rule [ A u P t (v := u) (B := A) (w := u) ] ⊢ J A u P t v (eq_refl B w) =⇒ t.
These equalities are only used to help elaboration figure out implicits in the right-hand side of the rule. They bear no meaning on the rewrite rule itself. For J, this is not a problem, because all well-typed instances of the left-hand side will actually verify these identities, but it is not a guarantee in general. Take for instance the following symbol and rule:

Symbol f : ∀ b, if b then N else B. Rewrite Rule [ b := true ] ⊢ f b =⇒ 23.
The rule will even trigger for the term f false meaning that we have something of type B which reduces to 23, a violation of subject reduction: the rule is simply not type preserving. We will now see that with universes we can run into more subtle problems with respect to type preservation.

Universes and Cumulativity. As exposed before, one major difference between Coq and Agda is the treatment of universes. In Coq, cumulativity means that sharing a common type for the left-hand side and the right-hand side (i.e., the requirement to postulate their propositional equality) is not sufficient to ensure type preservation, even when the rules are confluent. 3 A counter-example would be the following :

Symbol id : Type@{v} → Type@{u}. Rewrite Rule [ ] ⊢ id Type =⇒ Type@{u}.

Both sides share the super type Type@{1 + max u v}, but no constraints are inferred from the definition of the rule: it works for any level v and u. In particular it can be used to map terms of type Type@{u+1} to Type@{u}. This allows the user to create a term U : U when they might have thought assuming Type → Type was harmless. Not only does this break subject reduction, but also consistency. This raises two challenges to overcome: (1) theoretically we have to come up with a modular criterion to ensure type preservation of the typing rules; (2) in practice we need to be able to collect universe constraints not only on the symbol declaration but also in the rewrite rules themselves.

Reduction Strategies. Coq also features several reduction strategies such as call-by-value (cbv), call-by-name (cbn) or call-by-need (lazy), which are furthermore highly parametrisable (e.g., they can unfold constants or not). Naively grafting a function that matches left-hand sides of rules on top of one of these reduction machines will often lead to incompleteness issues:

(1) one has to ensure that subterms (function arguments) are in weak-head-normal form before matching them, which is not the case by default with cbn or lazy; (2) a function argument brought to normal form, when substituted into another term, may create a deep redex if the pattern is itself deep, which may cause problems with cbv. This means that we need to be careful when adding rewrite rules to those, otherwise users may face the frustration of having to type cbn several times to fully evaluate redices in a term.

In fact, we believe that proving such properties about reduction strategies would be nice additions to the MetaCoq project. One final challenge we have to face when dealing with rewrite rules in MetaCoq is that we do not know a priori that the rules do not break strong normalisation, while the current implementation and verification in MetaCoq relies on this assumption [SBF + 20]. We plan to solve this problem simply by no longer relying on this assumption. Instead, we believe that we can first define the reduction machine and the type checker as partial functions so that we may prove correctness on all terminating inputs, using ideas similar to the Braga method [START_REF] Larchey | The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq[END_REF].

Available at https://github.com/yannl35133/coq/tree/rewrite-rules-TYPES, examples can be found in the test-suite/success/rewrule.v file.

Available at https://github.com/yannl35133/metacoq/tree/rewrite-rules-TYPES


Kateryna Goloviznina

Ezzoubair Bendadesse

Jean-Marie Tarascon

Mathieu Salanne
email: mathieu.salanne@sorbonne-universite.fr

Ozlëm Sel

Ozlem Sel

Disclosing the Interfacial Electrolyte Structure of Na-Insertion Electrode Materials: Origins of the Desolvation Phenomenon

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

cathode materials for SIBs. [START_REF] Shen | Na+-Activation Engineering in the Na3V2(PO4)3 Cathode with Boosting Kinetics for Fast-Charging Na-Ion Batteries[END_REF] Their advantages include high redox potential due to the unique inductive effect of the polyanionic groups, high thermal stability, and robustness of the structural framework during intercalation/deintercalation processes that guarantees long life cycling, while as a main drawback, their low electrical conductivity is considered. [START_REF] Yabuuchi | Research Development on Sodium-Ion Batteries[END_REF][START_REF] Goikolea | Na-Ion Batteries-Approaching Old and New Challenges[END_REF][START_REF] Jin | Polyanion-type cathode materials for sodium-ion batteries[END_REF] The most common representative is Na 3 V 2 (PO 4 ) 3 (NVP), which has a theoretical capacity of 117 mA h g -1 and a plateau at 3.4 V corresponding to the V 3+ /V 4+ redox reaction. [START_REF] Cheng | Na3V2(PO4)3/C•Na3V2(PO4)2F3/C@rGO blended cathode material with elevated energy density for sodium ion batteries[END_REF] Going beyond the NaSICON family, a further increase of the redox potential in the Na-insertion electrode compounds can be achieved by introducing electronegative anions, such as F -, OH -, etc., into the NVP, which perturb the covalent bond between the transition metal and oxygen atoms. [START_REF] Jin | Polyanion-type cathode materials for sodium-ion batteries[END_REF] Therefore, by replacing one phosphate group with fluorine anions, forming Na 3 V 2 (PO 4 ) 2 F 3 (NVPF), one can attain a two high voltage plateau at 3.6 V and 4.2 V. [START_REF] Yang | High performance cathode material based on Na3V2(PO4)2F3 and Na3V2(PO4)3 for sodium-ion batteries[END_REF] The choice of the electrolyte remains crucial for the performance of SIBs. [START_REF] Ponrouch | Towards high energy density sodium ion batteries through electrolyte optimization[END_REF][START_REF] Ponrouch | Nonaqueous electrolytes for sodium-ion batteries[END_REF][START_REF] Heinz | NC-ND 4.0 Interfaces of Face-Centered Cubic Metals Using[END_REF] The most common way is to use a solution of sodium salt in an organic solvent, following the strategy of LIBs, though flammability and lack of safety stay an issue. [START_REF] Yan | A New Electrolyte Formulation for Securing High Temperature Cycling and Storage Performances of Na-Ion Batteries[END_REF] A typical example is a NaPF 6 , NaClO 4 , or NaBF 4 salt dissolved in a carbonate solvent. Cyclic carbonates such as propylene carbonate (PC) or ethylene carbonate (EC) have a relatively high dielectric constant that favors the dissociation of a salt, while their linear analog such as dimethyl carbonate (DMC) are often used as co-solvents to reduce the viscosity and ameliorate ionic conductivity of a system. [START_REF] Hijazi | Non-Aqueous Electrolytes for Sodium-Ion Batteries: Challenges and Prospects Towards Commercialization[END_REF] The carbonates remain the first choice also because of the formation of a highly stable solid-electrolyte interphase (SEI) that protects anode from the direct interaction with the solution. [START_REF] Hwang | Sodium-ion batteries: present and future[END_REF][START_REF] Muñoz-Márquez | Structure, Composition, Transport Properties, and Electrochemical Performance of the Electrode-Electrolyte Interphase in Non-Aqueous Na-Ion Batteries[END_REF] Alternatively, ionic liquids [START_REF] Gomes Chagas | Ionic Liquid-Based Electrolytes for Sodium-Ion Batteries: Tuning Properties To Enhance the Electrochemical Performance of Manganese-Based Layered Oxide Cathode[END_REF] and aqueous [START_REF] Liu | Water-Locked Eutectic Electrolyte Enables Long-Cycling Aqueous Sodium-Ion Batteries[END_REF] electrolytes can be used, but they do not lack disadvantages: the ILs usually possess high viscosities compared to conventional organic solvents that tend to increase even further upon the addition of a salt, [START_REF] Yang | Ionic liquids and derived materials for lithium and sodium batteries[END_REF] while the aqueous electrolytes have a narrow voltage stability window. [START_REF] Kim | Aqueous Rechargeable Li and Na Ion Batteries[END_REF] While the majority of studies focus on the Na + diffusion in the Na-insertion materials and the unit cell breathing upon intercalation, [START_REF] Chotard | Discovery of a Sodium-Ordered Form of Na3V2(PO4)3 below Ambient Temperature[END_REF][START_REF] Bianchini | Na3V2(PO4)2F3 Revisited: A High-Resolution Diffraction Study[END_REF][START_REF] Bui | Hybrid functional study of the NASICON-type Na3V2(PO4)3: crystal and electronic structures, and polaron-Na vacancy complex diffusion[END_REF][START_REF] Wang | Concerted Ion-Exchange Mechanism for Sodium Diffusion and Its Promotion in Na3V2(PO4)3 Framework[END_REF][START_REF] Song | First exploration of Na-ion migration pathways in the NASICON structure Na3V2(PO4)3[END_REF][START_REF] Broux | Temperature Dependence of Structural and Transport Properties for Na3V2(PO4)2F3 and Na3V2(PO4)2F2.5O0.5[END_REF][START_REF] Park | Crystal Structure of Na2V2(PO4)3, an Intriguing Phase Spotted in the Na3V2(PO4)3-Na1V2(PO4)3 System[END_REF] the cathode-electrolyte interfacial structure remains underinvestigated. Nevertheless, the arrangement of the solvent at the electrode sur-face affects ion desolvation and its migration from the bulk toward the interface, known to be an important energy-consuming step. [START_REF] Abe | CC BY-NC-ND 4.0 Between Graphite and Electrolyte[END_REF][START_REF] Abe | Lithium-Ion Transfer at the Interface Between Lithium-Ion Conductive Ceramic Electrolyte and Liquid Electrolyte-A Key to Enhancing the Rate Capability of Lithium-Ion Batteries[END_REF] For example, the energy barrier of Li + desolvation in an interphase-free LiPF 6 /EC-DMC/Li 4 Ti 5 O 12 measured by electrochemical impedance spectroscopy reaches about 12 kcal mol -1 . [START_REF] Xu | Differentiating Contributions to "Ion Transfer"Barrier from Interphasial Resistance and Li+ Desolvation at Electrolyte/Graphite Interface[END_REF] Of course, extensive experimental studies are barely possible for scanning a vast range of electrolyte compositions combined with different electrode types, and theoretical methods such as classical molecular dynamics (MD) are indispensable for the rational design of electrode-electrolyte systems. [START_REF] Jeanmairet | Microscopic Simulations of Electrochemical Double-Layer Capacitors[END_REF] In recent work, we combined electrochemical quartz crystal microbalance and operando infrared fiber evanescent wave spectroscopy with MD to study the operation of Na-insertion materials-based SIBs. [START_REF] Bendadesse | Spotting Interface Structuring during Na-Insertion into the NaSICON Na3V2(PO4)3 by EQCM and Operando Fiber Optic Infrared Spectroscopy[END_REF] We showed that upon insertion, a depletion of desolvated Na + occurs at the interface, which can impact the rate capability of the batteries, and may be generic to other types of solvent/ionic species. [START_REF] Lemaire | Probing the Electrode-Electrolyte Interface of a Model K-Ion Battery Electrode -The Origin of Rate Capability Discrepancy between Aqueous and Non-Aqueous Electrolytes[END_REF] Here we complement this work through the use of extensive MD simulations. We shed light on the local structure of 1 M NaPF 6 electrolyte in several organic carbonates (DMC, PC, and EC-DMC mixture (1:1 by molar fraction)) at the NVP and NVPF electrode surfaces, which will be compared to that at a graphite electrode.

Note that although SIBs generally employ hard carbon as the anode, the local structure of graphite provides a good model for the interface with the electrolyte. We demonstrate that the packing of a solvent at an electrode surface due to solvent-electrode interactions appears as one of the determining factors defining the activation barrier of the desolvation process.

Methods

Molecular dynamics simulations were performed using the LAMMPS program. [START_REF] Plimpton | Fast Parallel Algorithms for Short-Range Molecular Dynamics[END_REF] Initial configurations and input files were generated using Packmol, 41 VESTA 42 and fftool 43 The graphite electrode (GR) was represented by a hexagonal P 6 3/m m c space group [START_REF] Trucano | Structure of graphite by neutron diffraction[END_REF] and consisted of 3 layers of 34.08×36.89 Å size each. The NVP electrode was represented by a rhombohedral R -3 c space group, which is mostly always been reported in the literature, [START_REF] Zatovsky | NASICON-type Na 3 V 2 (PO 4 ) 3[END_REF][START_REF] Ghosh | High Capacity and High-Rate NASICON-Na3.75V1.25Mn0.75(PO4)3 Cathode for Na-Ion Batteries via Modulating Electronic and Crystal Structures[END_REF][START_REF] Chen | Activating a Multielectron Reaction of NASICON-Structured Cathodes toward High Energy Density for Sodium-Ion Batteries[END_REF] though Masquelier et al. [START_REF] Chotard | Discovery of a Sodium-Ordered Form of Na3V2(PO4)3 below Ambient Temperature[END_REF][START_REF] Park | Crystal Structure of Na2V2(PO4)3, an Intriguing Phase Spotted in the Na3V2(PO4)3-Na1V2(PO4)3 System[END_REF] mention several times the existence of a monoclinic distortion at ambient temperature. The slab had a size of 34.92 × 30.24 × 21.65 Å. The [001] plane of NVP was exposed toward the solution, following the recommendations from the literature. [START_REF] Chotard | Discovery of a Sodium-Ordered Form of Na3V2(PO4)3 below Ambient Temperature[END_REF] The crystal structure of the NVP comprised two types of Na + ions, shown in Figure 2a, the occupancy of which varied from one reference to another. [START_REF] Chotard | Discovery of a Sodium-Ordered Form of Na3V2(PO4)3 below Ambient Temperature[END_REF][START_REF] Zatovsky | NASICON-type Na 3 V 2 (PO 4 ) 3[END_REF][START_REF] Ghosh | High Capacity and High-Rate NASICON-Na3.75V1.25Mn0.75(PO4)3 Cathode for Na-Ion Batteries via Modulating Electronic and Crystal Structures[END_REF][START_REF] Chen | Activating a Multielectron Reaction of NASICON-Structured Cathodes toward High Energy Density for Sodium-Ion Batteries[END_REF] In order to match the experimental composition, we removed Na1 and Na2 ions only from the bulk of the electrode and not from the surface, which allowed us to avoid the intercalation of Na + ions from the solution to the solid. The NVPF electrode was represented by a tetragonal P 42/m n m space group, [START_REF] Meins | Phase Transitions in the Na3M2(PO4)2F3 Family (M=Al3+, V3+, Cr3+, Fe3+, Ga3+): Synthesis, Thermal, Structural, and Magnetic Studies[END_REF] with the [001] plane exposed towards the solution, similarly to the NVP case.

The slab had a size of 36.19 × 36.19 × 19.96 Å. The crystal structure contained two types of Na + ions, with the occupancy of 1.0 for Na1 and 0.5 for Na2, respectively (Figure 2b (left)). Since the distance of the closest Na2 sites is too short (1.865 Å), two neighboring Na2 sites cannot be simultaneously occupied due to the strong Coulomb repulsion between Na + ions. [START_REF] Shakoor | A combined first principles and experimental study on Na3V2(PO4)2F3 for rechargeable Na batteries[END_REF] Therefore, we had to remove half of Na2 atoms from the NVPF surface, and the resulting structure is given in Figure 2b (right). In all cases, a gold counter-electrode was used. It was represented by a cubic Fm-3m space group [START_REF] Suh | High-temperature thermal expansion of six metallic elements measured by dilatation method and X-ray diffraction[END_REF] with the [100] plane exposed to the solvent. The slab had a thickness of 12.22 Å, while its x and y dimensions were adjusted to fit those of NVP or NVPF. The Na + cation was represented by Aqvist force field, [START_REF] Ȧqvist | Ion-water interaction potentials derived from free energy perturbation simulations[END_REF] while the parameters of the PF - 6 anion were taken from the CL&P model. [START_REF] Lopes | Modeling Ionic Liquids Using a Systematic All-Atom Force Field[END_REF]53 The net charge of the ions was kept integer. The intermolecular interaction parameters of the electrode atoms, given in Table 1, were considered from several sources. [START_REF] Heinz | NC-ND 4.0 Interfaces of Face-Centered Cubic Metals Using[END_REF][START_REF] Ȧqvist | Ion-water interaction potentials derived from free energy perturbation simulations[END_REF][START_REF] Cole | The interaction between noble gases and the basal plane surface of graphite[END_REF][START_REF] Gupta | Force-field parameters for vanadium ions (+2, +3, +4, +5) to investigate their interactions within the vanadium redox flow battery electrolyte solution[END_REF][START_REF] Murzyn | Refined OPLS All-Atom Force Field Parameters for n-Pentadecane, Methyl Acetate, and Dimethyl Phosphate[END_REF][START_REF] Horinek | Rational design of ion force fields based on thermodynamic solvation properties[END_REF] The bonded and non-bonded parameters of solvent atoms were taken from the OPLS-AA, [START_REF] Jorgensen | CC BY-NC-ND 4.0 OPLS All-Atom Force Field on Conformational Energetics and Properties of Organic Liquids[END_REF] except for the partial charges, which were computed using the CHelpG procedure 59 on electron densities obtained at the MP2/cc-pVTZ level of theory at previously optimized geometries with the Gaussian16 program. The solvent models were validated by computing the densities and viscosities of bulk 1 M NaPF 6 solutions in the DMC, EC-DMC, and PC systems, which were compared to the experimental values. The simulation box was periodic in the x and y directions and a slab of 3 × L z was considered along the z direction. A cutoff of 12 Å was applied for non-bonded interactions. The particle-particle particle-mash (PPPM) method was used to evaluate electrostatic energies (the accuracy of 10 -5 ), with the slab correction taken into account. Both electrodes were considered immobile. Bonds terminating with hydrogen atoms were constrained using the SHAKE algorithm. The time step was set to 1 fs. The Nosé-Hoover thermostat was used to keep the temperature of the electrolyte solution at 298 K. Each system was equilibrated for 5 ns in the NVT ensemble and then a 50 ns production run was performed. The data analysis was performed using TRAVIS [START_REF] Brehm | TRAVIS -A Free Analyzer and Visualizer for Monte Carlo and Molecular Dynamics Trajectories[END_REF][START_REF] Brehm | TRAVIS-A free analyzer for trajectories from molecular simulation[END_REF] and our self-written tools. The visualization of the simulation box was done in VMD. [START_REF] Humphrey | Visual molecular dynamics[END_REF] The potentials of mean force (PMF) were calculated from separate runs, during which a single Na + ion was pulled from the solution towards the electrode surface. For this, a harmonic biasing potential varying between 25 kcal mol -1 Å -2 and 150 kcal mol -1 Å -2 was applied to this Na + ion. The z distance between the ion and the top surface atoms (C for graphite and Na for NVP and NVPF) was considered as the biasing collective variable. It was sampled between 12 Å and -2 Å with a step of 0.25 Å with 100 ps equilibration and 400 ps acquisition at each separation. The PMFs were calculated using the umbrella sampling and the weighed-histogram analysis method (WHAM). [START_REF] Kumar | The weighted histogram analysis method for free-energy calculations on biomolecules. I. The method[END_REF][START_REF] Grossfield | WHAM: the weighted histogram analysis method[END_REF] From the PMF trajectories, the coordination numbers of Na + as a function of its distance to an electrode were calculated. The coordination number cutoff was set to 4.55 Å for P of PF - 6 and 3.20 Å for O atoms of the carbonyl group of carbonate molecules, being defined as the position of the first minimum of the corresponding radial distribution functions of bulk systems. The coordination number curves were averaged over 3-6 replicas.

3 Results and discussion We first analyze the structure adopted by the solvent molecules at the various interfaces.

Density profiles (Figure 3), which provide information on the probability of finding species as surface (Figure S1a), so that the C O vector points away from the surface, marked by a greenish spot at about 4.8 Å O-surface separation (Figure 4a). This peak can be attributed to the solvent-electrolyte interactions as has been proposed by Borodin et al. [START_REF] Steinrück | [END_REF] in their study of LiPF 6 /EC-DMC/graphite by the surface-sensitive Ångstrom resolution X-ray reflectivity and molecular dynamics simulations. A lower probability but wide spot is observed at about 3.2 Å, which corresponds to the parallel orientation of the C O vector with respect to the surface plane. The ratio between these two peaks should depend on the electrolyte concentration in the solution. [START_REF] Steinrück | [END_REF] The second and further solvent layers are not clearly marked due to the conformation flexibility of DMC, which results in a variety of possible orientations.

The behavior of neat DMC solvent appears to be quite similar (Figure S2a). On the contrary, the EC molecules of the mixture are mainly oriented parallelly to the surface (corresponding to α = 90 • , shown in Figure 4b), at the O...surface separation of 3.2 Å. In addition to this, a low probably perpendicular orientation is observed at 6.6 Å distance. In the case of neat PC (Figures S2b), this perpendicular orientation does not emerge, being replaced by two peaks at 6.5-7.5 Å with a tilted orientation of the C O vector. The second solvent layer of parallelly oriented carbonate molecules is well-defined both for EC in the mixture and the neat PC.

The arrangement of solvent molecules at the NVP surface is strikingly different from that at graphite. The NVP slab, used for simulations, was cut in a way so that the PO 3- 4 and the Na + ions are exposed to a solution. We considered it the most likely case because the direction of the highest Na + diffusion in the solid [START_REF] Chotard | Discovery of a Sodium-Ordered Form of Na3V2(PO4)3 below Ambient Temperature[END_REF] is now aligned with the z axis of our simulation box. The top sodium ions of the NVP is then considered as a reference (z = 0) for the corresponding density profiles. A prominent peak between the top Na + ions of the surface and O atoms of the carbonyl groups is observed at about 2.15 Å in all solvents (Figures 3c-d).

The high intensity of this peak points to a tight packing of the solvent molecules near the electrode. The orientation of the C O vector with respect to the surface plane is strictly perpendicular (Figures 4c-d and Figures S3c-d). For DMC in the EC-DMC mixture, several As was mentioned before, this notable fraction of solvent molecules oriented toward the bulk solution can be explained by the interactions with the NaPF 6 salt. In the case of graphite (Figure 5a), Na + ions are mainly found at about 7.1 Å from the electrode in the DMC and EC-DMC solutions, and at 8.6 Å in PC, being followed by several low-intensity peaks at larger separation. Since no tight solvent layer is present near the electrode, the Na + ions can approach the graphite even closer, being noticed at 4.4-4.8 Å separations. At the NVP electrode (Figure 5b), which exhibits strong solvent adsorption, an intense Na + peak is observed just after the first solvent layer, at about 9. -f).

While the sodium cation is small and densely charged, the PF - 6 anion is remarkably larger; it thus displays a lower charge density. Therefore, it is mainly located just after the first solvent layer at about 7.7 Å, 9.0 Å and 8.8 Å from the graphite, NVP and NVPF surfaces, respectively (Figure 5d-f). In all the solvents, the peak is high and well-defined due to the large anion size, which also allows us to clearly identify the second and sometimes third anionic layers, especially when neat rigid PC is used as a solvent. Similarly to the Na + cations, the PF - 6 anions can also approach the graphite surface closer, down to distances of about 4.2 Å, while no similar effects are observed in the NVP and NVPF cases.

The potential of mean force (PMF), the free energy profile as a function of the distance of a Na + ion relative to the electrode surface, can provide complementary information to 13 https://doi.org/10.26434/chemrxiv-2023-7d7tz ORCID: https://orcid.org/0000-0002-1753-491X Content not peer-reviewed by ChemRxiv. License: CC BY-NC-ND 4.0 the solvent arrangement. [START_REF] Dubouis | Tuning water reduction through controlled nanoconfinement within an organic liquid matrix[END_REF][START_REF] Dorchies | Controlling the Hydrophilicity of the Electrochemical Interface to Modulate the Oxygen-Atom Transfer in Electrocatalytic Epoxidation Reactions[END_REF] Here, as a reference (z = 0), the distance corresponding to the minimum of each PMF is taken, being different from the density profile plots discussed earlier. Since there is no free energy barrier in approaching a Na + ion to the graphite surface in DMC or EC-DMC (Figure 6a), it can easily penetrate the closest solvent layer to the surface. This observation is consistent with the works of Hwang et al. [START_REF] Boyer | Structure and Li+ ion transport in a mixed carbonate/LiPF6 electrolyte near graphite electrode surfaces: a molecular dynamics study[END_REF] and Vatamanu et al. [START_REF] Vatamanu | Molecular Dynamics Simulation Studies of the Structure of a Mixed Carbonate/LiPF6 Electrolyte near Graphite Surface as a Function of Electrode Potential[END_REF] on LiPF 6 /EC-DMC/graphite system. On the contrary, a barrier of about 4.5 kcal mol -1 is observed in PC, probably related to a rigid geometry of the solvent molecules. This is reflected in the small prepeaks in density profiles, shown in Figure 5a, when the probability of observing a Na + ion near the surface is lower in neat PC than in other solvents. Due to the absence of specific sites at the graphite surface, capable of attracting the cation, it can freely move along and across the surface and move back to the bulk solution. Only in the case of PC, the barrier of about 3 kcal mol -1 should be overcome. In opposition to graphite, the NVP surface (Figure 6b) tends to form a firm solvent layer. In all the solvents, the free energy barrier attains about 20-25 kcal mol -1 . Once a cation reaches the NVP surface, it stays trapped there, being coordinated by three oxygen atoms of neighboring PO 3- 4 groups, so that it is placed on the top of V atoms. The free energy of diffusing back to the solution appears to be too high (90-120 kcal mol -1 ) to conquer.

The solvent layer at the NVPF surface is less tight, and the energy barrier achieves only 7-10 kcal mol -1 . The most probable adsorption site is in the hollow at the surface, being bounded by two oxygen atoms of PO 3- 4 groups. In such a case, the cation starts to penetrate the electrode, and further investigation of this process becomes out of the scope of classical MD. Alternatively, Na + ions can be absorbed on the top of P atoms, stabilized by interaction with two oxygen atoms (Figure S4), when no hollow site is available nearby.

The origin of the free energy barrier rises from the partial desolvation of a Na + ion when it approaches the electrode, penetrating through a tight first solvent layer. This can be confirmed by tracking the coordination number of a single Na + ion moving towards the surface. Figure 7 (as well as Figure S5) shows that, indeed, no desolvation is observed for the graphite, while the Na + cation loses its solvation shell when approaching NVP and NVPF. When comparing different materials, the firmness of solvent packing at a carbonatebased solvent at the electrode surface is greater at the NVP than at the NVPF, which actually explains the difference in the energy barriers: highly oriented solvent molecules at the interface require a higher energy contribution to change their configuration to solvate the diffusing Na + ion. In our recent EQCM study of the same systems under electrochemical cycling, [START_REF] Bendadesse | Spotting Interface Structuring during Na-Insertion into the NaSICON Na3V2(PO4)3 by EQCM and Operando Fiber Optic Infrared Spectroscopy[END_REF] we observed a detectable mass loss right before the insertion of Na + ions related to the desolvation only at the NVP, while in the case of NVPF, due to loose packing, the desolvation process remains confined within the penetration depth of the resonator's acoustic wave, thus cannot be detected as a mass loss.

Quantitative and even qualitative comparison with literature data remains problematic since the value of the activation barrier depends on a diversity of factors. In addition, no data for Na + -based systems have been reported to this point. Abe et al.

Conclusions

To sum up, the diffusion of a Na + ion through the electrolyte solution towards the cathode is strongly dependent on the surface nature. The nanostructure of the closest solvent layer at the interface defines the height of the activation barrier, commonly associated with the desolvation process. The desolvation does not seem to be observed at the SEI-free graphite electrode due to the absence of specific directional interaction between the solvent and the carbon sheets. On the contrary, because of the surface inhomogeneity and the presence of donor and acceptor groups, the polyanionic Na-insertion compounds exhibit a notable arrangement of solvent molecules in the closest layer, penetrating through which a Na + ion partially loses its solvent shell. The effect is the most pronounced at the NVP, which demonstrates the greatest energy barrier among studied systems as a result of the highly ordered and well-oriented first solvent layer. The solvent arrangement at the NVPF surface is slightly less marked due to the presence of non-polar fluorine atoms which partially disturb the solvent-electrode electrostatic attraction.

The nature of the solvent also plays an important role, but only when different families of solvents are compared. In our carbonate series, the variation between solvents (namely, due to the partial charge distribution) is quite subtle being a less significant factor than the electrode material. Even so, the lack of flexibility of the solvent impacts the tightness of its packing at the surface, which can lead to an increase in the activation energy barrier.

  figurations and input files were generated using Packmol, 41 VESTA 42 and fftool43 utilities.The simulation box consisted of two electrodes, separated by a 1 M solution of NaPF 6 in DMC, EC-DMC (1:1 molar fraction) or PC solvent. As electrode sets, graphite-graphite, NVP-Au and NVPF-Au pairs were considered. In total, 9 different systems were modelled.

Figure 1 :

 1 Figure 1: Simulation snapshot of the 1 M NaPF 6 /DMC electrolyte in contact with the NVP (left) and gold (right) electrodes.

Figure 2 :

 2 Figure 2: Visualisation of the NVP (a) and NVPF (b) surfaces exposed to a solution. Grey and purple spheres represent the Na + ions with different occupation (denoted as Na1 and Na2). In the case of NVP, no Na1 and Na2 ions were removed from the surface. Instead, they were removed from the bulk electrode to match the corresponding occupation (not shown). In the case of NVPF, all Na1 ions were kept, and one of Na2 in each pair (b, left) was removed for the surface (b, right).

60

 60

6

  https://doi.org/10.26434/chemrxiv-2023-7d7tz ORCID: https://orcid.org/0000-0002-1753-491X Content not peer-reviewed by ChemRxiv. License: CC BY-NC-ND 4.0

Figure 3 :

 3 Figure 3: Density profiles of O atoms (of the C O carbonyl group) of solvents in 1 M solution of NaPF 6 in the EC-DMC mixture (a,c,e) and DMC, PC solvents (b,d,f), as a function of their distance from the graphite (a,b), NVP (c,d), and NVPF (e,f) electrodes. As a reference (z = 0), the top carbon layer of graphite and the top sodium ions of the NVP and NVPF are considered, as illustrated by the inset.

Figure 4 :

 4 Figure 4: Probability contours revealing the orientation of the DMC and EC components in the 1 M NaPF 6 /EC-DMC solution with respect to the electrode surface. The x-axes represent the distances between the electrode (top C for the graphite, top Na for the NVP and NVPF considered as a reference) and the O atoms of the carbonyl group of a solvent. The y-axis represents the angles formed by the normal vector to an electrode plane and the C O vector of a solvent, as illustrated by the inset.

Figure 5 :

 5 Figure 5: Density profiles of Na + ions (a-c) and P atoms (d-f) of the 1 M NaPF 6 salt in DMC, PC solvents (a-c), and the EC-DMC mixture (d-f) as a function of their distance from the graphite (a,d), NVP (b,e), and NVPF (c,f) electrodes. As a reference (z = 0), the top carbon layer of graphite and the top sodium ions of the NVP and NVPF are considered.

2 - 9 . 4 Å

 294 . In the case of neat DMC, it is split into three smaller peaks (at 8.3 Å, 9.4 Å and 11.4 Å) due to multiple configurations of the flexible DMC molecule (Figures S3c), but the integral under them match that in EC/DMC and PC. At the NVPF surface (Figure 5c), the Na ions are distributed in the range of the 6.8-13.6 Å separations, with a principal peak at about 8.2-8.6 Å due to several dominant orientations of solvent molecules in the first layer(Figures 4e-f and Figures S3e

Figure 6 :

 6 Figure 6: Potential of mean force of approaching a single Na + ion to the graphite (a), NVP (b), and NVPF (c) electrode in different solvents. As a reference (z = 0), the minimum of each PMF is considered, corresponding to the most energetically favorable position of the Na + ion, as illustrated by the simulation snapshots.

Figure 7 :

 7 Figure 7: Total coordination number of solvent and anion species around a Na + cation moving towards the electrode surface in the NaPF 6 /EC-DMC solution. As a reference (z = 0), the minimum of each PMF given Figure 6 is considered. The coordination number values are averaged over several replicas.

Table 1 :

 1 Non-bonded interaction parameters of electrodes

	Graphite	C	0	3.330	0.2300	54
	NVP, NVPF Na	+1	3.330	0.0120	51
		V	+3	2.673	0.0602	55
		P	+5	3.740	0.1400	56
		O	-2	3.150	0.1700	56
		F	-1	3.440	0.4600	57
	Gold	Au	0	2.951	22.1334	19

Electrode

Atom type q / e -σ / Å ϵ / kJ mol -1 Ref.

  [START_REF] Abe | CC BY-NC-ND 4.0 Between Graphite and Electrolyte[END_REF][START_REF] Yamada | Kinetics of Lithium Ion Transfer at the Interface between Graphite and Liquid Electrolytes: Effects of Solvent and Surface Film[END_REF] measured the activation barriers of LiClO 4 salt in DMC and EC DMC (1:1 by vol.) at graphite by electrochemical impedance spectroscopy, and the variation between solvents (9.6 kcal mol -1 and 13.8 kcal mol -1 for DMC and EC DMC, respectively) was explained by the lower solvation ability of DMC than that of EC. However, changing the nature of the SEI almost vanished the difference between the two solvents. In our theoretical model, no SEI is present and no barrier is observed for NaPF 6 in these two solvents near graphite. Nevertheless, the height of the free energy barrier (when present) should also depend on the nucleophilic properties of a solvent. In their experimental study of a SEI-free LiPF 6 /Li 4 Ti 5 O 12 system, Xu et al.[START_REF] Xu | Differentiating Contributions to "Ion Transfer"Barrier from Interphasial Resistance and Li+ Desolvation at Electrolyte/Graphite Interface[END_REF] showed that an ether-based electrolyte had lower desolvation energy (by about 3 kcal mol -1 ) than carbonates. By modelling the diffusion of a Li + ion towards LiCoO 2 in PC and water, Nikitina et al.[START_REF] Chekushkin | -ND 4.0 overestimated role of desolvation[END_REF] also obtained rather different values: 10.4 kcal mol -1 and 5.8 kcal mol -1 , respectively. For our DMC -EC/DMC -PC carbonate series, the difference between solvents' donor ability is too delicate to be captured by simulations: partial changes of O solvent atoms are quite close and no explicit lone pairs are present. Therefore, the solvent packing at the interface appears to play the principal role in defining the height of the activation barrier.

https://doi.org/10.26434/chemrxiv-2023-7d7tz ORCID: https://orcid.org/0000-0002-1753-491X Content not peer-reviewed by ChemRxiv. License: CC BY-NC-ND 4.0

https://doi.org/10.26434/chemrxiv-2023-7d7tz ORCID: https://orcid.org/0000-0002-1753-491X Content not peer-reviewed by ChemRxiv. License: CC BY-NC-ND 4.0

Acknowledgement

This work was funded by the European Research Council (ERC) under the European Union Horizon 2020 research and innovation program (grant agreement 771294). Computational tasks were performed using resources from GENCI-IDRIS (Grants 2022-A0120910463 and 2023-A0140910463) and from the MeSU supercomputer of Sorbonne University.

Supporting Information Available

Density profiles, probability contours, simulation snapshots, and coordination number plots.