Roberto Blanco
email: roberto.blanco@inria.fr

Zakaria Chihani
email: zakaria.chihani@cea.fr

An interactive assistant for the definition of proof certificates

Keywords: focused proof system, foundational proof certificate, proof checking

The Foundational Proof Certificate (FPC) approach to proof evidence offers a flexible framework for the formal definition of proof semantics, described through its relationship to focused proof systems. The certificates thus produced by tools are executable when interpreted on top of a suitable logic engine, and can therefore be independently verified by trusted proof checkers.

The fundamental obstacle encountered here lies in translating the proof evidence produced by a tool in the terms of a formal definition in the system. These formal definitions are akin to domain-specific languages (in which proofs can be written) programmed in the assembly language of the underlying proof systems: a delicate task for which both expert knowledge and great care are needed.

To facilitate broader adoption, we begin to explore techniques that abstract away part of this complexity and bring the FPC framework closer to a user-friendly, programmable platform in which a wide range of high-level certificate definitions can be easily encoded.

Introduction

The notion of proof as a document that attests to the truth of a certain mathematical property finds ample support in the ever-growing myriad of software tools that facilitate the production and verification of such entities: automated theorem provers, proof assistants, model checkers, programming languages, etc. However, there remain fundamental issues of what constitutes acceptable proof evidence of the truth of a statement; how such information should be presented and communicated; and how its foundations can be assessed, deemed to be compatible with a certain logical framework, and, possibly, reused: questions the proliferation of tools and standards, as well as reasoning frameworks, only exacerbates. Some exchange format standards have arisen and are in wide use [START_REF] Sutcliffe | The TPTP problem library and associated infrastructure[END_REF], but the critical gap between the syntax and the semantics of proof evidence remains [START_REF] Blanco | Defining the meaning of TPTP formatted proofs[END_REF].

In response to this situation, Dale Miller and colleagues have developed a general framework for the expression of proof evidence in the form of Foundational Proof Certificates (henceforth, FPCs) [START_REF] Miller | Communicating and trusting proofs: the case for foundational proof certificates[END_REF]. Central to this paradigm is the notion of certificate: a document of which, given a suitable definition, acts as a universal representative of a proof, which exists independently of any and all tools -however central software is to the production and treatment of these. Under this discipline, a separation of concerns is established in the dichotomy of the prover, responsible for producing proofs in the form of FPCs, and the checker, in charge of their independent verification. The proof checker, then, elaborates a certificate into a formal proof. The following four desiderata synthesize the fundamental requirements of such a program.

1. A simple checker can, in principle, check if a proof certificate denotes a proof.

2. The format for proof certificates must support a wide range of proof options.

3. A proof certificate is intended to denote a proof in the sense of structural proof theory. [START_REF] Blanco | Defining the meaning of TPTP formatted proofs[END_REF]. A proof certificate can simply leave out details of the intended proof.

Harnessing recent advances in proof theory, crystallized in the form of various focused proof systems [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF] and their metatheories, these requirements have been shown to be well within reach. These systems become the "rules of chemistry" which enable us to naturally and efficiently take "atoms" of inference and compose them into more complex, higher-level "molecules" of inference. FPCs offer a general framework to define and describe proofs in a certain logic, regardless of provenance, and verify their truthfulness by means of a checker that embodies the aforementioned "rules," in terms of which the certificates are ultimately expressed. The remarkable fact that universal checkers that embody these rules can and should be technically simple and their correctness easy to ascertain, even formally, naturally creates a delegation of responsibilities, in which the burden of correctness is lifted from the shoulders of the complex programs that are provers, and trust in the overall process increases, among other benefits.

There remains the practical question of adoption as a practical standard for communication used by software provers. As will be expounded in following sections, the expressive power of FPCs and the capabilities of proof checkers have been studied through a number of implementations and definitions of the semantics of a range of representative proof evidence. However, the translation of the complex, heterogeneous, ad hoc proof formats of the many provers of interest in the common language of FPCs presents us with a substantial technical challenge.

The theoretical foundations of proof certificates have been compared with the basic rules of chemistry in their proposals. We liken them, rather, to a fantastic new assembler, one that programs a machine that is based purely on logic. The definition of the semantics of a certain proof certificate -which we have previously characterized as PRICEs [START_REF] Chihani | Certification of first-order proofs in classical and intuitionistic logics[END_REF] -essentially specifies a domain-specific language in which proof evidence of a theorem can be expressed: the concrete certificate that contains this information acts as a program written in the language of the PRICE and interpreted on the checker that implements the assembly of the chosen architectural logic. The analogy is apt insofar as it reflects the deep ties to the intricacies of the proof systems: so far, programming these PRICEs has been the delicate domain of the expert, and while ground has been broken in the connection between concrete proof assistants and suitable logics, it is laborious to extend these results to arbitrary proving software, commonly closer to the proof normalization of functional programming than to the proof search that is native to this effort -in contrast with Dedukti, [START_REF] Boespflug | The λΠ-calculus modulo as a universal proof language[END_REF] which endeavors to solve similar questions through different methods.

For Foundational Proof Certificates to fulfill their potential, we believe it is necessary to develop for them a full-fledged discipline of programming. In this way, they can cease to be the exclusive domain of the logician, and be understood and used by the authors of the various families of theorem proving tools, thus becoming easily integrated in them and paving the way for the communication of proofs between tools that is one of the goals of this research effort. We find this a pragmatic and necessary goal, and set out to commence its development in this paper.

The rest of the paper is organized as follows. Section 2 furnishes an introduction to the FPC framework and presents the systems for classical logic that will be employed a means of illustration and experimentation. Section 3 discusses the current state of FPC programming: the problem domains to which it has been successfully applied to date, and the required methodology, as well as the limitations of this approach. In response to these, Section 4 proposes an assistant to simplify, and make the creation and maintenance of PRICEs more robust and accessible to non-specialists; Section 5 describes a prototype implementation, codenamed sunshine, that encodes these precepts in a simple, meaningful logical framework. Finally, Section 6 discusses further developments that we consider necessary in the technical evolution of FPCs as a discipline of wide reach and practical impact.

Foundational Proof Certificates

Focused sequent calculus

The "rules of chemistry" and "atoms of inference" referred to in Section 1 are precisely those of the sequent calculus, in which the proof system imposes no restrictions whatsoever on the shapes of proofs. With the addition of focusing, proofs are decomposed in alternating asynchronous and synchronous phases, which constitute a first element of order in the otherwise chaotic sequent calculus. Miller's desiderata guided the design of a framework for Foundational Proof Certificates, which will be introduced now. The presentation will be centered on Gentzen's classical calculus LK, and its focused variant LKF [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF].

Consider the proof system in Figure 1, where all annotations in blue are disregarded: this is the system LKF. A focused system operates on polarized formulas, obtained from regular, unpolarized formulas by replacing each logical connective with a polarized version of it, positive or negative, and by assigning a polarity, again positive or negative, to each constant. In firstorder classical logic, the four connectives ∧ (conjunction), ∨ (disjunction), t (true), f (false) exist in both positive and negative polarities; the universal quantifier ∀ is always negative, whereas the existential quantifier ∃ is always positive. The polarity of a formula is that of its top-level connective. Formulas are always in negation normal form, so that the scope of negation is exactly atomic, and thus negation corresponds to a simple polarity flip. In the description that follows, by "formula" we will mean a polarized formula.

It is visible from the inference rules that constitute the calculus that sequents can be of two, distinct types, corresponding to the two kinds of phases.

1. Up-arrow sequents Γ ⇑ Θ, related to the asynchronous phase, where Γ is a multiset of formulas and Θ is a list of formulas. The rules of this phase are invertible and involve exclusively up-arrow sequents in both conclusion and premises. Due to this property, rules can be applied to saturation; by convention, in order from head to tail of the list Θ.

2. Down-arrow sequents Γ ⇓ B, related to the synchronous phase, where Γ is a multiset of formulas and B is a formula. Non-invertible rules are applied to a single formula, B, that is the focus of the phase, making local choices and introducing backtracking points as demanded by the rules, until no more actions avail.

In both classes of sequents, the left-hand side Γ represents a storage of formulas that exist in opposition to the workbench (respectively, Θ and B). Phase transitions are arbitrated through the structural rules, which move synchronous formulas to storage during the asynchronous phase and select ("decide on") one of these to focus on in the transition from asynchronous to synchronous (contraction), and release an asynchronous formula in the transition from synchronous to asynchronous. A final group of inference rules deals with identity (weakening) and cut. As proved by Liang and Miller, theoremhood of a formula B of LK is equivalent to provability of Asynchronous Rules

Ξ 1 Γ ⇑ Θ f c (Ξ 0 , Ξ 1 ) Ξ 0 Γ ⇑ f -, Θ Ξ 1 Γ ⇑ A, Θ Ξ 2 Γ ⇑ B, Θ ∧ c (Ξ 0 , Ξ 1 , Ξ 2 ) Ξ 0 Γ ⇑ A ∧ -B, Θ Ξ 1 Γ ⇑ A, B, Θ ∨ c (Ξ 0 , Ξ 1 ) Ξ 0 Γ ⇑ A ∨ -B, Θ Ξ 0 Γ ⇑ t -, Θ (Ξ 1 y) Γ ⇑ (B y), Θ ∀ c (Ξ 0 , Ξ 1 ) Ξ 0 Γ ⇑ ∀x.B, Θ † Synchronous Rules t e (Ξ 0 ) Ξ 0 Γ ⇓ t + Ξ 1 Γ ⇓ B 1 Ξ 2 Γ ⇓ B 2 ∧ e (Ξ 0 , Ξ 1 , Ξ 2 ) Ξ 0 Γ ⇓ B 1 ∧ + B 2 Ξ 1 Γ ⇓ B i ∨ e (Ξ 0 , Ξ 1 , i) Ξ 0 Γ ⇓ B 1 ∨ + B 2 Ξ 1 Γ ⇓ (B t) ∃ e (Ξ 0 , Ξ 1 , t) Ξ 0 Γ ⇓ ∃B Identity rules Ξ 1 Γ ⇑ B Ξ 2 Γ ⇑ ¬B cut e (Ξ 0 , Ξ 1 , Ξ 2 , B) Ξ 0 Γ ⇑ • cut l : ¬P a ∈ Γ init e (Ξ 0 , l) Ξ 0 Γ ⇓ P a init Structural rules Ξ 1 Γ ⇑ N release e (Ξ 0 , Ξ 1 ) Ξ 0 Γ ⇓ N release Ξ 1 Γ ⇓ P l : P ∈ Γ decide e (Ξ 0 , Ξ 1 , l) Ξ 0 Γ ⇑ • decide Ξ 1 Γ, l : C ⇑ Θ store c (Ξ 0 , Ξ 1 , l) Ξ 0 Γ ⇑ C, Θ store
P is a positive formula. N is a negative formula. P a is a positive literal. C is a positive formula or a negative literal. ¬B is the negation of B in negation normal form. The proviso † is the eigenvariable restriction that y must not occur free in Ξ, Θ, Γ, and B. the entry point sequent • ⇑ B, where • is the empty storage and B is an arbitrary polarization of B; moreover, the cut-elimination property holds in the system.

Augmenting the calculus

Consider now Figure 1 in its entirety. Each premise and conclusion in every inference rule has been enriched with a certificate term, Ξ. Moreover, an additional "premise" has been added to every rule -except the asynchronous rule for true. These premises relate the certificate term of the conclusion with the certificate terms, and any other necessary information, required by the premises to proceed with proof search: which branch of a disjunction to pick, which stored formula to select, how to instantiate an existential variable. In addition, the formula storage zone Γ becomes a multiset of indexed formulas. By furnishing declarations (syntax) and definitions (semantics) to these extensions, certification is enabled.

Because LKF is sound and complete and all these extensions can accomplish is either enabling or disabling certain inference rules based on the certificate term in their conclusion, one can prove directly, by erasure of these restrictions, that soundness is preserved. What we gain is a powerful discipline that brings order into the maelstrom of indiscriminate proof search.

The semantics of an FPC definition, which describes a family of certification strategies, is what we call PRICE. There are five groups of elements that constitute a PRICE. 1. Polarization. A polarization strategy determines how to move from unpolarized formulas to their polarized versions (the other direction is direct by erasure). As we have seen, the choice of polarities by itself does not affect provability, but its interactions with the other members of a PRICE may. Despite this seeming leniency, the role of polarities should not be underestimated: they have a strong impact of the proofs that can be found for a given theorem, and can represent the difference between exponential, brute force search and intent, efficient navigation along a predetermined proof path.

2. Certificate terms (the "R(egions)" of a PRICE). Conceptually, certificate terms represent the state, or the region of a proof in which we find ourselves at a given point in the derivation. As this state changes, so do the certificates, and the information contained in them can be used to steer the derivation towards success.

3. Indexes. As synchronous formulas are moved to the storage zone Γ, they are annotated with data contained in an index term, supplied in the store rule. Like certificate terms, they may contain arbitrary information, and can later be called upon to selectively retrieve a subset of candidate formulas for selection by the decide rule. Lookup can be as loose or as tight as the designer chooses, offering great control over backtracking.

4.

Clerks. These predicates, denoted by the c subscript in Figure 1, define the control semantics of asynchronous rules. While not explicitly responsible for the decisions that are characteristic of synchronous rules, they can nonetheless perform bookkeeping that will eventually enable their counterparts to make their decisions when their time comes. These can be thought of as ordinary program clauses, making full use of the power of logic programming.

5.

Experts. The synchronous counterparts of clerks, signified by the e subscript, are like their asynchronous duals arbitrary program clauses, but in addition to possibly recording information while processing certificate terms they will be required to make the decisions demanded by their phase. How much or how little they commit to one or several possible courses of action is not dictated by the framework and remains purely a design issue.

Identity rules take place during the synchronous phase and are therefore supervised by experts. Structural rules are more nuanced: store occurs during the asynchronous phase and is assigned a clerk, although it is charged with the critical operation of filing formulas into storage, in the process assigning them indexes. In turn, decide arbitrates the transition from asynchronous to synchronous phase by using those very indexes, and its complement release mediates the other phase transition. Both these transitions can be seen as operating "between two worlds," and are here both declared as experts.

λProlog implementations of both the LKF system augmented with the FPC framework, named LKF a , are available as kernels. These are direct translations of the proof system and, if one is willing to trust an implementation of a logic programming language, deeming such a kernel trustworthy as well should be fairly simple.

3 Programming FPCs in the small

Development in practice

Even as we guide users away from the cryptic assembly of the sequent calculus, letting them instead write abstract certificate terms based on a PRICE, the establishment of a mapping between these abstract terms and their correspondence with the assembly level is an inevitable step of significant complexity that needs to be repeated, with variations, for each FPC definition. Despite this, the applicability of the framework to a number of representative and highly varied settings has been studied with satisfactory results. Among these, proof formats for classical and intuitionistic first-order logic, are studied at length in [START_REF] Chihani | A semantic framework for proof evidence[END_REF], and the examples in this section are derived from here. A proof theoretic vision of model checking is possible if a richer logic is selected; µM ALL, i.e., multiplicative-additive linear logic with greatest and least fixed points as logical connectives instead of exponentials, is suitable for this purpose [START_REF] Heath | A framework for proof certificates in finite state exploration[END_REF]. In a similar vein, the addition of fixed points to intuitionistic logic, µLJ, serves to reason about constructive proofs and their expression as outlines, in a note closer to the connection between theorem provers and certification [START_REF] Blanco | Proof outlines as proof certificates: a system description[END_REF]. It is possible to treat modal logics like K as well, and a focused version of the labeled sequent system based on it, G3K; this system can then be utilized to certify modal tableaux [START_REF] Libal | Certification of prefixed tableau proofs for modal logic[END_REF]. Logic programming is the natural environment for these developments. Kernels and proof checkers are built in λProlog [START_REF] Miller | Programming with higher-order logic[END_REF], or Bedwyr [START_REF] Baelde | The Bedwyr system for model checking over syntactic expressions[END_REF] when fixed points are needed.

Commonly, an approximate idea of the end result exists in the mind of the designer from the outset, subject to refinements and generalizations. In practice, testing plays an essential role to confirm, at least empirically, that a PRICE satisfies its intended semantics. In spite of its practical importance, the support offered by the usual programming environments is rather basic, as are debugging facilities. Even working around this, it must be remembered that to date few formal guarantees of a semantic correspondence are routinely obtained. Anecdotal evidence suggests that is is possible for seemingly small changes to break examples that previously worked, and better support to avoid these regressions would be desirable: the augmented proof systems ensure soundness, but reaching and maintaining completeness (relative to the proof strategy of interest) is the sole domain of the designer, and currently evaluated mainly by way of test cases.

The rest of the section is dedicated to two elementary examples of uses of the framework. It will become clear that this methodology of programming is still very close to the logic, and expert domain knowledge is required to harness its expressive power; even then, judging by our experience, the process is far from straightforward. We present these as motivation to develop past these early stages and into a truly formal methodology. The interactive assistant will take some first steps in that direction.

Example: a decision procedure

An extreme minimalist use of the FPC framework is studied in this subsection. Consider the propositional fragment of the logic where everything is negatively polarized. In this situation, there is no opportunity to offer guidance during the synchronous phase, and our only recourse is to exhaustive search. While completely blind and impossibly inefficient, it is clearly a sound, if empty, strategy, a fact that can be clearly represented with a PRICE, describing its parts as follows. of complementary polarities, e.g., negated atoms are given negative polarity; non-negated atoms are given positive polarity. This is the only allowed use of positive polarity.

2. Certificate terms carry no information. A singleton, nullary constructor (cnf) leaves no option but to propagate it from conclusion to premises.

3. Indexes carry no information, either. A singleton, nullary constructor (idx) is assigned to all formulas in storage and decided on. The storage zone acts as a bucket devoid of any clues to help us decide on the appropriate formula: each decision will be attempted on each and every formula in Γ.

4.

Clerks are declared for the negative connectives to enable proof search to proceed through them and store positive formulas and negative literals, i.e., atoms, without distinction.

5.

Experts are declared only for phase transitions, vacuously, and for the init rule, to allow an atom to be matched with its stored complement and close the branch. It can be seen that, by design, the other inference rules cannot occur, and therefore their definition would have no effect in proof search.

Adopting a simple naming standard and encoding of arguments from conclusion to premises and left to right, we obtain the PRICE in Figure 2.

With patience, the theoremhood of small propositional formulas can now be checked by using cnf with the entry point sequent.

Example: binary resolution

It is instructive to see how the core of a standard proof technique can be encoded in the framework. To this end we turn to resolution refutations. Here we want to attempt to prove a formula of the form ¬C 1 ∨ . . . ∨ ¬C n , with each clause C i a disjunction of literals closed by universal quantifiers. The key idea of the technique lies in the binary resolution rule (here, Ls represent literals of either polarity).

L 1,1 ∨ • • • ∨ L 1,i-1 ∨ P a ∨ L 1,i+1 ∨ • • • ∨ L 1,m L 2,1 ∨ • • • ∨ L 2,j-1 ∨ ¬P a ∨ L 2,j+1 ∨ • • • ∨ L 2,n L 1,1 ∨ • • • ∨ L 1,i-1 ∨ L 1,i+1 ∨ • • • ∨ L 1,m ∨ L 2,1 ∨ • • • ∨ L 2,j-1 ∨ L 2,j+1 ∨ • • • ∨ L 2,n
A proof operates by attempting to apply the rule to a pair of clauses to generate a new clause, until the empty clause f is reached, at which point the refutation is concluded with success. By assigning names to the clauses that compose the formula to be proved, as well The initial certificate of a proof attempt by resolution must encode this information. Assuming clause names are natural numbers assigned incrementally and starting from one, an obvious possibility is this triple.

1. A list of clauses corresponding to the C 1 , . . . , C n of the formula whose proof will be attempted. These will receive identifiers 1 through n.

2.

A list of clauses used in the proof but not included in the input clauses, i.e., derived by applications of the resolution rule on previous clauses. These will receive identifiers starting from n + 1.

3. A list of triples of numeric indexes i, j, k, where i and j are the indexes of the premises and k the index of the conclusion of the rule.

In order to design the PRICE in detail, we determine one possible shape of a general proof by resolution in LKF a , and work around to sculpt it during proof search. A detailed description can be found, e.g., in [START_REF] Chihani | A semantic framework for proof evidence[END_REF]. Conceptually, a proof is divided in three main region types:

1. The first phase operates asynchronously storing the clauses that configure the potential theorem under their respective indexes. The encoding is shown in Figure 3.

2. The second phase connects each use of the resolution rule with a use of cut. One of the branches of this cut will continue on to the next instance of the resolution rule, forming a backbone of cuts that culminates in the empty clause. The encoding is shown in Figure 4.

3. The third phase (type) constitutes the proof of the other branch of each cut of the second phase, and is responsible for checking that the resolution rule on the triple of indexes specified by the certificate is, indeed, correct. The encoding is shown in Figure 5.

It is clear from even a cursory analysis that an interesting certificate such as this, compact and relatively simple, depends deeply on the proof system and the conventions it establishes during the design of a general "proof scaffold." Preconditions must be carefully documented, but irrespective of this, and while the framework provides facilities for abstraction, the process remains delicate and difficult to scale. Let this illustration motivate the sections that follow.

Towards programming in the large

Patterns of abstraction

As exemplified in Section 3, PRICE definitions have been the result of careful analysis of the logical structure of proofs in relation to a suitable, focused proof system expressed in terms of the sequent calculus. They range in complexity from the simplest decision proceduresexponential on the size of the input -to sophisticated methods of proof reconstruction that encode precise instructions to guide proof search; the size of certificates, too, varies widely. The programming environment of choice is generally that of higher-order logic, e.g., λProlog or Bedwyr.

A common observation that arises from most of the more sophisticated certificate definitions, and many moderately complex ones, is that they can be fairly brittle in their behavior: they will certainly work under the exact conditions for which they were designed, but will fail unexpectedly if presented with seemingly minor variations on the basic problem structure considered during programming; of the examples considered, resolution is a particularly apt example. Even simple definitions, such as imposing bounds to the complexity of proofs based on depth can present limited, if unexpected, complexity in managing the regions of the proof in an exact manner. These issues originate in the conceptual distance between the high-level states and translations determined by the algorithms that define decision procedures, and the low-level sequents and inference rules of the sequent calculus. These latter must be orchestrated by a PRICE to produce an equivalent behavior. This, embedded in a powerful logic programming environment, results in systems whose behavior can be laborious to diagnose and debug.

The keys to reducing the complexity involved in the handcrafting of a certificate definition are abstraction and automation. There are two fundamental, compatible strategies to hiding the complexity that underlies the framework: one can attempt to expose the logic minimally, hiding aspects of the inner workings of the proof system that are inessential to the end user; on the other hand, there has to be a core of the programming interface, describing the instructions that guide proof search, that can never be neglected: simplifying its use is the second alternative. A minimal proficiency with logic must be assumed, and in the early stages of the development of a system like we propose this level must be, as a minimum, close to the logic of choice, while the minutiae of its underlying proof system become less critical with successive refinements. Two measures to guide access to the logic itself, not the framework, are apparent.

1. Choice of logic. If the user has selected a logic to target their problems, they will be prompted to state so. Otherwise, an assistant will ask a few questions about their formulas to determine if the system supports a suitable logic, either directly or by means of a mapping. Other options, such as inferred or explicit polarities, below, will have a bearing on the dialog with the user.

2. Choice of polarity. Among the five components of a PRICE, only polarity is part of the proof system proper; the other four parameters instantiate the FPC framework and are considered separately. The choice of polarity depends on various considerations. Especially common among these are the following:

(a) All connectives involved in a clause representing a deterministic computation must be negative. (b) Formulas to which a contraction rule may be applied, i.e., through the decide rule, must be therefore positively polarized. (c) Polarization criteria for atoms (and, conversely, for their negations) are not strictly necessary in classical logic, but have a profound influence on the shape of the proofs whose derivation they may allow.

As in the choice of logic, a user who has knowledge of polarities and their behavior can choose to select the allowed subset of polarized connectives. Otherwise, an attempt at inferring the adequate polarities can be made from such questions about the nature of the envisioned proofs as have are being considered here. Where there are degrees of freedom left, the various possibilities could be explored through interactive examples.

Once these parameters are fixed, the user needs to define indexes to store and decide on formulas, certificate constructors to represent the state of proof reconstruction, and the clauses of clerks and experts that encode the transitions between states for each inference rule allowed under the constraints imposed by the above steps. The facilitation of this labor is principally technical in nature. Constructor parameters can be declared and supplied to the clauses, choices restricted to syntactically correct values, and some decisions made automatically based on the current signature. On top of all this syntactic assistance, the definition of semantics falls ultimately on the user. Therefore, whereas the benefits of abstraction are limited to a simplified interface to the FPC API, those of automation can significantly simplify programming, especially for non-specialists.

Workflow overview

sunshine is an interactive PRICE definition assistant. Its purpose is to guide and supervise the design of a certificate definition, from its contact surface with logic to the domain-specific language in which certificates will be written. It does not assume or require familiarity with the FPC framework, although acquiring this will be a natural consequence of controlled exposure to the sequent calculus.

The model of computation for the assistant is an adaptation of the REPL pattern that incrementally builds a PRICE, modified in part by some static restrictions of the logic, and by those programmed dynamically by the user. The system starts with a blank slate and gradually builds a functional FPC definition, while never allowing false steps to be taken. It is an assistant in that it maintains and makes explicit all possible decisions that can be taken at any one time in the context of the logical framework, helps the user to state their intent and requests the necessary information while shielding them as much as possible -or desired -from implementation details. To do this, it is structured along the following components integrated in an activity loop.

1. Logic selection. Subject to an optional guidance procedure, selects the corresponding kernel implementing the proof system for the logic of choice, along with the logic programming environment that forms the basis for the runtime. In addition, an empty signature for the proof system is loaded and made available to the refinement loop.

2. Restrictions on focusing. Any restrictions imposed either manually or through an inference procedure limit some of the options that are offered through the refinement loop, namely those regarding the available inference rules and, with them, the types of clerk and expert clauses that may be defined. (In particular if there are unresolved ambiguities, a related procedure could be integrated in the miscellaneous processing of the loop, although we will not pursue this possibility in the present treatment.)

3. Refinement loop. Once a logical frame of reference has been established, and the logical component of the PRICE determined, the user enters a REPL loop within which they can proceed to iteratively define the components of an FPC and experiment with them interactively. Each step offers several possibilities to extend the definition, while the system ensures that the PRICE remains in a consistent state, if possibly incomplete, thus minimizing the inadvertent accumulation of errors. A number of basic steps can be chosen from.

(a) Definition of certificate or index terms. Before any clerk or expert clauses can be defined, the signature must contain some constructors for certificates and, in all likelihood, indexes. Each of these will have an arity, and each argument a type from the signature. (b) Ancillary signature declarations. In order to supply information to both certificate and index constructors, and manipulate this information in the clerk and expert clauses, it will be necessary in all but the most trivial certificates (cf., e.g., Figure 2) to extend the signature with new kinds and type constructors, in much the same way as certificate and index terms are defined. (c) Definition of clerk or expert clauses. Based on the contents of the signature (types, constructors) and the restrictions placed by focusing on the sequent calculus, the user can select from a list of possible end-sequents corresponding to each possible inference rule, and edit (create, update, delete) the clauses assigned to the clerk or expert for the inference rule. Pure transformations based on pattern matching can be fully guided with ease, and the user need not be exposed to the programming language and kernel under the hood. However, clerks and experts in complex PRICEs may carry out computation, and for this "dropping down" to the programming language level is the only option that offers sufficient generality to be currently considered. (d) Ancillary clauses. Complex FPC definitions of the kind described in the last category may require the declaration of arbitrary propositions and clauses outside the interface of the framework. For this, as above, the only possibility that is currently envisioned is through direct programming in the core language. (e) Validation and miscellaneous subprocesses. After each step, the evaluation must include various checks to ensure that the revised PRICE remains in a consistent state, alerting the user of any problematic attempts, as well as serving as a watchdog against bugs in the assistant itself. We consider these facilities in following subsections.

(Additionally, the tool could evolve to offer an extension interface to allow the writing of customized modules to enrich the functionality of the software.) (f) Import/export. At any moment, the user must be capable of exporting the current state of the assistant into a full-fledged, executable PRICE, and restore the state from a previous session, or from any other means through which an FPC definition can be created, including programming directly against a kernel without an assistant. Specially formatted annotations are used to communicate information specific to the assistant, such as any desired restrictions on focusing, as already discussed. These must include any extrinsic source of information used by the validation subprocesses that does not directly depend on the FPC framework itself.

The process continues for as long as the user desires, and can be interrupted or restored at any time. There are some dependencies on runtime systems that must be maintained, with relative ease. More interesting are the internal dependencies of the growing PRICE. The interactive loop encourages a certain incremental approach that maintains consistency at all times. However, changes in definitions, like the parameters of a certificate constructor which has been used in the definition of clerks and experts, cannot be performed in one basic step of the loop. As in the general practice of programming, there are no trivial solutions for cascading errors, and if substantial alterations are required it is always possible to export the PRICE, perform the modifications and re-import and validate the modified version. Other alternatives will be discussed shortly.

Static analysis

The fundamental component of the validation sub-step of the main activity loop is charged with ensuring that user changes introduce no inconsistent states. In first instance, this requires validating the signature and typechecking the "program," i.e., the instantiation of the kernel where calls to clerks and experts are filled in with the definitions given by the PRICE. It is possible, although inefficient, to "export" the FPC definition on the background, load it in the kernel, compile it against the core programming environment, and report any resulting errors. Moreover, error messages would need to be deciphered and references to the positions of errors back-translated and correlated with the user's input.

This general-purpose treatment covers those checks that are shared with the logic programming environment, but the assistant is not limited to these simple properties. An internal model of the signature and the general structure of the kernel enables more sophisticated processing that goes beyond the validation phase.

1. Recommendations and auto-fill. When writing a clause for a clerk or expert, the checker can explore the signature for compatible type constructors, and offer or default to filling out arguments automatically if a single possibility is found, otherwise it can offer a list of compatible constructors, and recurse into any arguments of these.

2. Flow analysis. The clerk and expert clauses correlate the transformations between certificate constructors, as well as the storage and retrieval of formulas through index constructors. This program does not exist in a vacuum: each clerk and expert is embedded in a specific inference rule of the kernel implementing the focused sequent calculus for the logic. This, coupled with the restrictions on focusing, which are, in fact, restrictions on the logic itself and its formulas, gives way to a rich category of analyses, of which the following general representative has been studied.

(a) Dependency graph. From the end-sequents and the possible transitions between them and to the init-like rules that end a branch of the derivation -noting that some of these rules inspect the certificate, while others discard it -, a dependency graph can conservatively determine whether certain certificate constructors constitute dead ends that cannot possibly lead to a successful proof. Parameters that are unused, or are passed without transformations or effects can be identified, as can index families that will become stale and not contribute to the process, based on their use by the store and decide rules.

3. Refactoring assistance. The static analyzer can present the user with additional operations, specifically consistent transformations on the current state of the PRICE, such as renaming, and introduction or removal of constructor parameters, with the possibility to supply or recommend default values for all affected instances, insert dummy placeholders, globally or locally, or traverse the program in an input sub-loop.

The lint-like tool that results can find useful applications not only embedded in the assistant, but as part of a reactive development environment that is decoupled from the framework, once the scaffolding of the FPC framework is factored in.

In addition to exploiting the restrictions on the program imposed by the FPC framework and the evolving FPC definition, further constraints can be coordinated with user-defined tests, which are the topic of the next subsection.

Testing

A final and no less critical component of the assistant facilitates the crucial requirement that the user be capable of writing certificates in the defined language that enable them to prove properties of interest. As observed in Section 3, tests give confidence that the defined certificates guide proof search along the desire paths. The FPC framework ensures the soundness of each and every PRICE, and the main task of the designer is to restrict the indiscriminate completeness of blind proof search to reflect the semantics of the proof format under consideration.

This feature reflects the mental process, akin to test-driven development, that guides the design of the PRICE and offers additional information to the static analyzer, pinpointing the sources of shortcomings in the program and even suggesting when it may be more lenient than necessary. We cannot assume tests to be satisfiable by simple changes: this is to say that adding a new test that covers unimplemented functionality is not considered an inconsistent step. Failing tests in the suite do not cause a failure in validation, but must nevertheless report that the current scope of a certificate definition is not yet complete.

Runtimes and programming languages support tests in varying degrees, and the assistant must therefore provide a unified interface to each targetable system. As with the simpler flavor of static analysis, it becomes necessary to instantiate the runtime system with the current state of the PRICE, execute it under controlled circumstances, and parse the output to report back on test results through the interface. Tests can be of two types.

1. Positive tests. Polarized formulas and certificates that must lead to a successful proof of the formula. They serve to ensure that the kernel does enough to find a proof.

2. Negative tests. Polarized formulas and certificates that must exhaust the search for a proof, given the constraints of the definition, without success. These are more natural to a model checking system like Bedwyr, but can be built with some extra work into the other environments (esp., λProlog), and are concerned with preventing the kernel from doing too much by limiting its expressive power.

With these facilities in place, the assistant has all the basic elements it needs to guide the user through the process of defining a PRICE from start to finish.

5 Architecture and design of the assistant

Backend

This section gives a brief overview of a prototype implementation of sunshine. The system can be neatly decomposed in a frontend, in charge of interactions with the user, and a backend that implements the core of the system and interfaces it with the FPC framework. This last piece of software is considered separate, trustable, and endowed with a standard API (exposed through a logic programming language) against which to program: this is prepared to encompass the set of supported runtime systems.

For the purposes of the present treatment, we make a number of simplifying assumptions that allow us to focus on the key aspects of the system.

1. Logic selection. A single proof system, LKF a , described in Section 2, is supported in its λProlog implementation. This determines the programming environment, so that while a layer of abstraction can be foreseen, efforts in modularity can be directed to other, more interesting areas. For this reason, it is possible to lift the restrictions of the "user language" (i.e., keywords, variable naming conventions, typing, etc.) directly from the "object language," in this case λProlog.

2. Restrictions on focusing. It will be assumed that the user has a basic knowledge of focusing and the focused proof system, so that inference of polarity becomes unnecessary. This will simplify somehow the static analysis, given that no external restrictions must be accounted for, and the full system is studied by default. This is an interesting feature to have, but its complexities are beyond the scope of a first incarnation of the software.

3. Refinement loop.

(a) Ancillary clauses. The full programming environment will not be exposed at this point, except through the importing of PRICEs processed by an external editor. External definitions will not be given through the assistant, though they may be imported, and clauses will be centered around pure, if possibly redundant, pattern matching. (b) Validation and miscellaneous subprocesses. Only static analysis and testing will be considered, with no support for external modules at this point.

Given these fortified requirements, the assistant jumps directly into the refinement loop, with all the necessary data structures to maintain the signature and state of the program, and the classes implementing the functionality of the various possible steps, fully instantiated with the logic, the kernel and the runtime of its implementation. Within the application, a main controller accepts commands from the user and dispatches them to the appropriate handlers, thus updating the state of the PRICE and performing all necessary checks. The user interacts with the controller through an interface. It can be observed that this application model fits well in the common model-view-controller (MVC) architectural design pattern, with only small adjustments.

As noted above, the language in which identifiers, program clauses, etc., will be written is standard λProlog, as implemented in Teyjus [START_REF] Nadathur | System description: Teyjus-a compiler and abstract machine based implementation of λProlog[END_REF]. Use of predefined types, predicates, and operators from the standard library is not allowed in the current, purely declarative setting based on inductive types and pattern matching, although a prefixed subset of identifiers is reserved for internal use by the assistant due to the rudimentary support for namespaces in the language. Translation from the data structures of the assistant to the target language, modular composition (i.e., instantiation of the kernel, execution of test cases) and management of batch jobs is handled through a separate utility class that is accessed by command modules as needed.

The implementation of such a proof of concept is not particularly sensitive to technological choices, and the basic algorithms it requires do not hide any extraneous sources of complexity. We think the merit of this design relies on its elegant integration in a conceptually simple but powerful framework.

Frontend and user interface

The frontend performs the function of views in the MVC model, and connect the actions of the user with the commands defined by the various controller classes. A local installation of the assistant and its dependencies can run in any Unix-like machine through a simple commandline interface. This CLI will present an overview of the current PRICE definition and allow display of all further details; it will display available options and query for choices; and it will compose the calls to the controllers, and display errors and return values from the invoked methods. While a simple linear dialog is possible, the task of displaying complex information is facilitated by the use of a terminal graphics library in the tradition of the curses family.

An appealing alternative that remains to be explored exploits the wide availability of modern MVC frameworks such as Django (for Python) or Ruby on Rails (for Ruby), which would replace the terminal with a web application, which in turn could be hosted by an external server, made available to researchers for experimentation without installation, and would be capable of producing more responsive, powerful interfaces. The logic programming environments exist outside these frameworks and present prospective servers with some additional, less mainstream requirements. However, recent experiments cross-compiling the proof assistant Abella -closely related to Bedwyr -to JavaScript and running it on the browser [START_REF] Chaudhuri | Abella in your browser[END_REF] show promise in relaxing these demands.

With this note, we conclude the description of the proof of concept. Assistant implementations will be made available from the ProofCert repositories. 1

Discussion

In foregoing pages we have proposed a definition assistant that streamlines the creation and maintenance of FPC definitions and improves existing analysis and testing techniques for the typical programming environments in which this activity takes place. It can serve as a learning tool not only applied to the FPC framework, but for the sequent calculus and logic programming more generally. By way of exercise, we may recommend to understand what it would take to recreate (redesign?) the example PRICEs in Section 3, and reflect on what this teaches us about the problems and the challenges presented to make this technology more usable and widely adopted.

Some obvious candidates for improvements come in the form of extensions to the assistant, i.e., both removing the simplifications and adding the possibilities for refinement that have been discussed in Sections 4 and 5. Some, like polarity inference, are of some theoretical interest, while many others are principally needed to evolve a mature tool that more users may be interested in using. These incremental advances push away from the details of the logic, but the disentanglement is never complete, and we do not think we should be satisfied with this state of affairs. One issue in particular remains unanswered: how to guarantee that a PRICE implements a semantics defined in terms other than those of the proof system? The semantics we refer to is known beforehand and corresponds to the proof method we wish to certify; it is not an artifact that may be discarded lightly. A further qualitative step to greater abstraction would pursue to hide the clockwork of sequent calculus as much as possible, and from the point of view of the user this would be ideal, but is dependent on establishing a more indirect link between semantics. This is an avenue we would like to explore in the future.

Also related to trust and correctness, scrupulous developers may want to consider whether there may be bugs lurking in the kernels that constitute the cornerstone of the system, and whose correctness has been taken as a matter of fact throughout the paper. Certified implementations of the various kernels, and even a more general framework for certification of these critically important pieces of code, would be steps in a right direction orthogonal to that of the correctness of semantics considered before.

Less lofty but useful goals also avail. Given that we would like to see greater support for the FPC framework in the corpus of verification software, it would be beneficial to explore adding total or partial support to representatives of this category, such as theorem provers. Abella [START_REF] Baelde | Abella: a system for reasoning about relational specifications[END_REF], a proof assistant based on logic that is closely related to Bedwyr, is a promising candidate that could pave the way for new developments in the interaction between standard proving tools and certification, including but not limited to adopting certificates as tactics, exporting certificates from native proof scripts.

To conclude, we reiterate our conviction that the theorem proving community would benefit greatly from the approach to certification advocated through the FPC framework. Protected by firm proof theoretical foundations, it remains to make these available to the larger scientific community, not only through advocacy, but by example as well. Making the framework attractive and easy to use is key to acquiring a critical mass of users that could bring it, and its benefits, closer to widespread use.

Figure 1 :

 1 Figure 1: The augmented LKF proof system LKF a

Figure 2 :

 2 Figure 2: A conjunctive normal form PRICE: full decision procedure

  type idx int -> index . type start int -> list method -> cert . orNeg_kc ( start C Resol ) ( start C Resol ). false_kc ( start C Resol ) ( start C Resol ). store_kc ( start C Resol ) ( start D Resol ) ( idx C ) :-D is C + 1.

Figure 3 :

 3 Figure 3: A binary resolution PRICE (1): store the negated clauses of the alleged theorem

Figure 4 :

 4 Figure 4: A binary resolution PRICE (2): a backbone of cuts that lead to the selection of the empty clause

Figure 5 :

 5 Figure 5: A binary resolution PRICE (and 3): check an individual resolution step by a shallow proof

Code repositories will be made publicly available after the celebration of DaleFest on 16 December

Acknowledgments. The authors cannot fail to express their gratitude to Dale Miller as the spring and inspiration for this project. They furthermore wish to thank Tomer Libal in special for helpful discussions and comments. This work has been funded by the ERC Advanced Grant ProofCert.


F Pellarin

A NOTE ON CERTAIN REPRESENTATIONS IN CHARACTERISTIC p AND ASSOCIATED FUNCTIONS

The aim of this note is to describe basic properties of the representations of GL2 (Fq[θ]) associated to certain vectorial modular forms with values in Tate algebras and Banach algebras introduced by the author. We discuss how certain L-values occur as limits values of these functions. We also present families of examples which can be the object of further studies. σ -→ Mat d×d (K),

Introduction

In [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF], the author has introduced some special functions related to the arithmetic of function fields of positive characteristic (and more precisely, to the arithmetic of the ring Fq[θ] with θ an indeterminate), namely, L-values and vector valued modular forms (the vectors having entries in certain ultrametric Banach algebras). The purpose of [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF] was to produce a new class of functional identities for L-values, and only very particular examples of these new special functions were required, in order to obtain the results in that paper. The theory was later developed along several axes (see for example [START_REF] Anglès | Arithmetic of positive characteristic L-series values in Tate algebras[END_REF], which also contains quite a detailed bibliography).

The aim of this note is to highlight the connection that these special functions have with representations of algebras, groups etc. associated to A, and to present families of examples which can be the object of further studies. In particular, we are interested in certain irreducible representations of SL2(Fq[θ]) or GL2 (Fq[θ]). We also provide a few explicit examples and properties of such representations.

The plan of the note is the following. In §2, we discuss algebra representations of A and we will consider their associated ω-values and L-values. In §3, we present a class of irreducible representations ρ I inside symmetric powers in the case q = p. In §4, we apply the results of §3 to show that certain tensor products ρ II are irreducible. In §5 we use these results to show that the entries of certain vectorial Poincaré series generalizing those introduced in [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF] are linearly independent and we present a conjecture on the rank of a certain module of vectorial modular forms.

In all the following, q = p e with p a prime number and e > 0. we set Γ = GL2(Fq[θ]), where q = p e for some prime number p and an integer e > 0. We shall write A = Fq[θ] (so that Γ = GL2(A)). All along the paper, if a = a0 + a1θ + • • • + arθ r is an element of A with a0, . . . , ar ∈ Fq and if t is an element of an Fq-algebra B, then a(t) denotes the element a0 + a1t + • • • + art r ∈ B. Also, we set K = Fq(θ).

Algebra representations

In this section, we consider an integral, commutative Fq-algebra A and we denote by K its fraction field. We denote by Matn×m(R), with R a commutative ring, the R-module of the matrices with n rows and m columns, and with entries in R. If n = m, this R-module is equipped with the structure of an R-algebra. We choose an injective algebra representation [START_REF] Anglès | Arithmetic of positive characteristic L-series values in Tate algebras[END_REF] A which is completely determined by the choice of the image ϑ := σ(θ). Note that σ is not injective if and only if ϑ has all its eigenvalues in F ac q , algebraic closure of Fq (In all the following, if L is a field, L ac denotes an algebraic closure of L). Further, we have that σ is irreducible if and only if its characteristic polynomial is irreducible over K.

2.1. An example. We denote by A[θ] + the multiplicative monoid of polynomials which are monic in θ. Let P be a polynomial in A[θ] + , let d be the degree of P in θ. The euclidean division in A[θ] by P defines for all a ∈ A[θ], in an unique way, a matrix σP (a) ∈ Mat d×d (A) such that aw ≡ σP (a)w (mod

P A[θ]),
where w is the column vector with entries 1, θ, . . . , θ d-1 . Explicitly, if

P = θ d + P d-1 θ d-1 + • • • + P0 with Pi ∈ A, then σP (θ) =        0 1 • • • 0 0 0 • • • 0 . . . . . . . . . 0 0 • • • 1 -P0 -P1 • • • -P d-1        .
Hence, the map σP defines an algebra representation

A σ P --→ End(A d ).
The representation σP is faithful if P has not all its roots in F ac q and is irreducible if and only if P is irreducible over K.

L-values

and ω-values of algebra representations and semi-characters. We give a few elementary properties of certain basic objects that can be associated to representations such as in [START_REF] Anglès | Arithmetic of positive characteristic L-series values in Tate algebras[END_REF]. Since the proofs are in fact obvious generalizations of the arguments of [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF][START_REF] Anglès | Arithmetic of positive characteristic L-series values in Tate algebras[END_REF], we will only sketch them.

For a ring R, we denote by R * the underlying multiplicative monoid of R (if we forget the addition of R we are left with the monoid R * ). We recall that A + denotes the multiplicative monoid of monic polynomials of A. Let M be an Fq-algebra (for example, M = Mat d×d (K) for some integer d).

Definition 1. A monoid homomorphism

σ : A + → M *
is a semi-character if there exist pairwise commuting Fq-algebra homomorphisms σ1, . . . , σs

: A → M such that, for a ∈ A + , σ(a) = σ1(a) • • • σs(a).
The trivial map σ(a) = 1M for all a is a semi-character, according to the convention that an empty product is equal to one. If, for all i = 1, . . . , s, ϑi = σi(θ) has a well defined minimal polynomial over K, we say that the semi-character σ is of Dirichlet type. This happens if, for example, M = Mat d×d (K). The conductor of a semi-character of Dirichlet type is the product of all the pairwise distinct minimal polynomials of the elements ϑ1, . . . , ϑs.

Example. If we choose M = F ac q , then a semi-character σ : A + → F ac q is always of Dirichlet type, and our definition coincides in fact with the usual notion of a Dirichlet-Goss character A + → F ac q . There are non-pairwise conjugated elements ζ1, . . . , ζs ∈ F ac q , of minimal polynomials P1, . . . , Ps ∈ A, such that σ(a) = a(ζ1) n 1 • • • a(ζs) ns for all a ∈ A, with 0 < ni < q d i -1 for all i, with di the degree of Pi. The conductor is the product P1 • • • Ps.

Non-example. We set M = Fq[x] and we consider the map σ : A + → M defined by a → x deg θ (a) . Then, σ is a monoid homomorphism which is not a semi-character. Indeed, assuming the converse, then σ = σ1 • • • σs for algebra homomorphisms σi : A → M . But since σ(θ) = σ1(θ) • • • σs(θ) = x, we get s = 1 and σ would be an algebra homomorphism, which is certainly false.

From now on, we suppose, for commodity, that M = Mat d×d (Ks) with Ks = Fq(t1, . . . , ts) (but some of the arguments also hold with M any Fq-algebra). Let K∞ be the completion of K = Fq(θ) at the infinity place. Then, K∞ = Fq((θ -1 )), with the norm | • | defined by |θ| = q (associated to the valuation v∞ such that v∞(θ) = -1). Let C∞ be the completion K ac ∞ , where K ac ∞ denotes an algebraic closure of K∞. We denote by Ks the completion of the field C∞(t1, . . . , ts) for the Gauss valuation extending the valuation of K∞, so that the valuation induced on F ac q (t1, . . . , ts) ⊂ C∞(t1, . . . , ts) is the trivial one. Also, we denote by Ks,∞ the completion of K(t1, . . . , ts) in Ks; we have Ks,∞ = Ks((θ -1 )). We have that K∞ = K0,∞, and K0 = C∞.

2.2.1. ω-values of an algebra representation. We consider a d-dimensional representation as in [START_REF] Anglès | Arithmetic of positive characteristic L-series values in Tate algebras[END_REF], in M = Mat d×d (Ks). We consider the following element of K∞ ⊗ Fq M = Matn×n(Ks,∞) ⊂ C∞ ⊗ Fq M = Matn×n(Ks), the topological product ⊗ Fq being considered with respect to the trivial norm over M . We denote by Πσ the convergent product

Πσ = i≥0 (I d -σ(θ)θ -q i ) -1 ∈ GL d (Ks,∞)
(where I d denotes the identity matrix). Let λ θ be a root (-θ)

1 q-1 ∈ K ac of -θ. The ω-value associated to σ is the product ωσ = λ θ Πσ ∈ GL d (Ks,∞(λ θ )).
We have, on the other hand, a continuous Ks-algebra automorphism τ of Ks uniquely defined by setting τ (θ) = θ q . By using an ultrametric version of Mittag-Leffler decomposition, it is easy to show that K τ =1 s , the subfield of Ks of the τ -invariant elements, is equal to Ks. We denote by τ the algebra endomorphism of Mat d×d (Ks) defined by applying τ entry-wise.

Lemma 2. The element ωσ is a generator of the free M -submodule of rank one of Mat d×d (Ks) of the solutions of the τ -difference equation τ (X) = (σ(θ) -θI d )X.

Proof. (Sketch.) It is easy to verify that ωσ is a solution of the above equation.

If ω ′ is another solution, then Y = ω ′ ω -1 σ is solution of τ (Y ) = Y in Mat d×d (Ks), hence, Y ∈ M .
Remark 3. It is also easy to prove that, for σ as in [START_REF] Anglès | Arithmetic of positive characteristic L-series values in Tate algebras[END_REF], det(ωσ) = ωα, where α ∈ Ks[θ] is -1 times the characteristic polynomial of σ(θ) and ωα is the function defined in [1, §6].

Let T be another indeterminate. The algebra Mat d×d (Ks) is endowed with a structure of A[T ]-module in two ways. The first structure is that in which the multiplication by θ is given by the usual diagonal multiplication, and the multiplication by T is given by the left multiplication by σ(θ); this defines indeed, uniquely, a module structure. The second structure, called Carlitz module structure, denoted by C(Mat d×d (Ks)), has the same multiplication by T and has the multiplication C θ by θ independent of the choice of σ, and defined as follows.

If m ∈ C(Mat d×d (Ks)), then C θ (m) = θm + τ (m).
We have the exponential map

exp C : Mat d×d (Ks) → C(Mat d×d (Ks)) defined by exp C (f ) = i≥0 D -1 i τ i (f ),
where Di is the product of the monic polynomials of A of degree i. It is quite standard to check that this is a continuous, open, surjective A[T ]-module homomorphism, of kernel π Mat d×d (Ks[θ]), where

π := θλ θ i>0 (1 -θ 1-q i ) -1 ∈ λ θ K∞ ⊂ C∞ is a fundamental period of Carlitz's exponential exp C : C∞ → C∞. Lemma 4. We have ωσ = exp C π(θI d -σ(θ)) -1 . Proof. We set f = exp C π(θI d -σ(θ)) -1 . Since (C θ -σ(θ))(f ) = 0 in C(Mat d×d (Ks))
, Lemma 2 tells us that f belongs to the free M -submodule of rank one of Mat d×d (Ks) of the solutions of the homogeneous linear difference equation described in that statement. Now, observe that

ωσ = θλ θ (θI d -σ(θ)) -1 + M1, f = θλ θ (θI d -σ(θ)) -1 + M2,
where M1, M2 are matrices with coefficients in Ks,∞ whose entries have Gauss norms < |λ θ | = q 1 q-1 . Hence ωσ = f . 2.2.2. L-values associated to a semi-character. we again suppose that M = Mat d×d (Ks), with Ks as in the previous sections. Let σ be a semi-character A + → M Let n be a positive integer. The n-th L-value associated to σ is the following element of GL d (Ks,∞):

Lσ(n) = P I d -σ(P )P -n -1 = a∈A + σ(a)a -n = I d + • • • ,
the product running over the irreducible elements of A + . 2.2.3. Determinant. We write σ = σ1 • • • σs for injective Fq-algebra homomorphisms σi : A → M with σi(θ), σj (θ) commuting each other. The elements Lσ(n) and ωσ 1 • • • ωσ s commute each other. Further we denote by λi,1, . . . , λ i,d ∈ K ac s the eigenvalues of σi(θ) for i = 1, . . . , s (considered with multiplicities). For simplicity, we suppose that none of these eigenvalues belong to F ac q . On the other hand, we consider variables x1, . . . , xs and the L-value: Proof. We note that, for every polynomial

Ls(n) := P (1 -ψs(P )P -n ) -1 , where ψ : A + → Fq[x1, . . . , xs] * is the semi-character defined by a → a(x1) • • • a(xs),
P ∈ A + , det((I d -σ(P )P -n ) -1 ) = P dn det(I d P n -σ(P )) -1 .
By the well known properties of the characteristic polynomial of an endomorphism, we have that

det(P n -σ(P )) = d i=1 (X -µi,P )X=P n ,
where µi,P ∈ K ac s are the eigenvalues of the left multiplication by σ(P ). Now, observe that

σ(P ) = s j=1 σj (P ) = s j=1 P (σj(θ))
(the elements σj (θ) commute each other). Hence, µi,P = s j=1 P (λi,j) for all i = 1, . . . , d. Thus, det(I d -σ(P )P -n ) -1 = P dn s j=1

I d P n - s j=1 P (λi,j) -1
, and the lemma follows.

2.2.4. The case n = 1. We write σ = σ1 • • • σs as above. Since for all a ∈ A + , Ca(ωσ i ) = σi(a)ωσ i ∈ M , we have the convergent series identity

a∈A + a -1 Ca(ωσ 1 ) • • • Ca(ωσ s ) = Lσ(1)ωσ 1 • • • ωσ s ∈ Mat d×d (Ks,∞(λ θ ))
(in fact, the series converges to an invertible matrix).

2.2.5. A Simple application of Anderson's log-algebraic Theorem. We now invoke the result of B. Anglès, F. Tavares Ribeiro and the author [1, Theorem 8.2] (note that in the statement, we can set Z = 1). For completeness, we mention the following result, which is a very easy consequence of ibid.: Proposition 6. For every semi-character σ :

A + → M with σ = σ1 • • • σs as above, (ωσ 1 • • • ωσ s ) -1 exp C (ωσ 1 • • • ωσ s Lσ(1)) =: Sσ ∈ Mat d×d (Ks[θ]).
Further, if s ≡ 1 (mod q -1) and if s > 1, the matrix with polynomial entries Sσ is zero. In particular, in this case,

Lσ(1) = π(ωσ 1 • • • ωσ s ) -1 Bσ,
where Bσ is a matrix with polynomial entries in Ks[θ].

Hence, Lσ(1) is a "Taelman unit", in the sense of [START_REF] Taelman | Special L-values of Drinfeld modules[END_REF]. If s = 1, we have a more explicit property. In this case, σ extends to an algebra homomorphism σ : A → M , and we have the simple explicit formula

Lσ(1) = ω -1 σ (I d θ -σ(θ)
) -1 π which can be proved in a way very similar to that of [7, §4]. We are going to see, in §5.2.1 that Lσ(n) is related to certain vectorial Eisenstein series, when n ≡ s (mod q -1).

2.3.

Representations of Γ associated to an algebra representation. Let K be any commutative field extension of Fq. Let σ be a d-dimensional representation as in [START_REF] Anglès | Arithmetic of positive characteristic L-series values in Tate algebras[END_REF]. We associate to it, canonically, a representation of Γ = GL2(A) in GL 2d (K).

We consider the map Γ Then, ρσ determines a representation Γ → GL 2d (K). Indeed, σ(a), σ(b) commute each other, for a, b ∈ A. Furthermore, we have:

Lemma 7. ρσ is irreducible if and only if σ is irreducible.

Proof. Let V be a non-trivial sub-vector space of Mat d×1 (K) such that σ(a

)(V ) ⊂ V . Then, if γ = ( a b c d ) ∈ Γ, we have ρσ(γ) = σ(a) σ(b) σ(c) σ(d) (V ⊕ V ) ⊂ V ⊕ V
and σ not irreducible implies ρσ not irreducible. Now, let us assume that σ is irreducible and let us consider V a non-zero sub-vector space of Mat 2d×1 (K) which is ρσ-invariant. We observe that

V ∩ ∆ = {0}, with ∆ = { v v : v ∈ Mat d×1 (K)}. Indeed, ρσ(( 0 1 1 0 )) = ( 0 I d I d 0 ) and ρσ(( 1 0 0 -1 )) = ( I d 0 0 -I d ). If x y is a non-zero vector of V with x = -y, we have x y +ρσ(( 0 1 1 0 )) x y = x+y x+y ∈ ∆\{0}. If x = -y, then ρσ(( 1 0 0 -1 )) x y ∈ ∆\{0}. Let v v be non-zero in V ∩∆. Since for all a ∈ A, ρσ(( 1 a 0 1 )) v v = ( I d σ(a) 0 I d ) v v = σ(a ′ )v v with a ′ = a + 1 we have { σ(a)(v) v : a ∈ A} ⊂ V . Let W be the K-sub-vector space of Mat d×1 (K) generated by the set {σ(a)(v) : a ∈ A}. Then, W is σ-invariant: if w = i ciσ(ai)(v) ∈ W (ci ∈ K, ai ∈ A), we have that σ(a)(w) = i ciσ(aai)(v) ∈ W.
By hypothesis, W is non-zero, so that W = Mat d×1 (K). We have proved that V ⊃ Mat d×1 (K) ⊕ {v}. Translating, this means that V ⊃ Mat d×1 (K) ⊕ {0}. Applying ρσ(( 0 1 1 0 )) we see that V ⊃ {0} ⊕ Mat d×1 (K) and V = Mat 2d×1 (K).

Example. We can construct, in particular, the representation ρP = ρσ P : Γ → GL 2d (A) which is irreducible if and only if P is irreducible.

Symmetric powers

In the first part of this section, we suppose that q is a prime number; p = q. Let B be an Fp-algebra. We denote by ρ the tautological representation GL2(B) → GL2(B). We consider the representation

ρr = Sym r (ρ) : GL2(B) → GLr+1(B),
where Sym r denotes the r-th symmetric power realized in the space of polynomials homogeneous of degree r + 1 with coefficients in

B. If γ = ( a b c d ) ∈ GL2(B), then ρr(γ)(X r-i Y i ) = (aX + cY ) r-i (bX + dY ) i , i = 0, . . . , r.
Associated to an integer l ≥ 0 with p-expansion l = l0 + l1p + • • • + lsp s (0 ≤ li ≤ p -1), we also consider the representations

ρ I l = ρ l 0 ⊗ ρ (1)
l 1 ⊗ • • • ⊗ ρ (s)
ls , where, for a matrix M with entries in B, M (i) denotes the matrix obtained from M raising all its entries to the power p i . The dimension of ρ I l is equal to

φp(l) = i (li + 1).
Lemma 8. The representation ρ I l is isomorphic to a sub-representation of ρ l .

Proof. We actually construct the sub-representation explicitly; the Lemma will follow easily. We consider, for γ ∈ GL2(B), the matrix ρ ⋆ l (γ) which is the square matrix extracted from ρ l (γ) = (ρi,j) 1≤i,j≤l+1

in the following way. If 0 ≤ r ≤ l is such that l r ≡ 0 (mod p), we drop the (r + 1)-th row and the (r + 1)-th column. In other words, one uses the row matrix

D l = l l , . . . , l r , . . . , l 0
and discards rows and columns of ρ l according with the vanishing of the corresponding entry of D l and what is left precisely defines the matrix ρ ⋆ l . By Lucas formula, ρ ⋆ l has dimension φp(l) and it is easy to see, by induction on the number of digits of the p-expansion of l, that ρ ⋆ l ∼ = ρ I l .

Example. If l = 1 + p, we have

D I l = (1, 1, 1, 1) = l 0 , l 1 , l p , l l .
In this case, we find, for γ = ( a b c d ),

ρ ⋆ l (γ) =     a p+1 a p b ab p b p+1 a p c a p d b p c b p d ac p bc p ad p bd p c p+1 c p d cd p d p+1     .
Remark 9. We notice the following algorithm to construct the sequence of dimensions (φp(l)) l≥1 . Define a0 = (1), a1 = (1, 2, . . . , p) (equal to the concatenation [a0, 2a0, . . . , pa0]) and then, inductively, an = [an-1, 2an-1, . . . , pan-1].

Since it is clear that for all n, an-1 is a prefix of an, there is a well defined inductive limit a∞ of the sequence (an) n≥0 which is easily seen to be equal to the sequence (φp(l)) l≥1 .

3.1. Representations of SL2(F q ′ ). Let us set q ′ = p f with f > 0. Then, B = F q ′ is an Fp-algebra and we can construct the representations ρ l and ρ ⋆ l ∼ = ρ I L of the beginning of this section. We denote by ρ l the representation ρ I l with B = F q ′ restricted to SL2(B). By using the fact that any non-zero stable subspace in a representation of a p-group over a vector space has a non-zero fixed vector, it is easy to show and in fact well known that, for all l ≥ 0, ρ l is an irreducible representation if and only if l < q ′ . By Schur's theory, one shows that the representations ρ l with l < q ′ exhaust all the isomorphism classes of irreducible representations of SL2(F q ′ ) over F ac p . Indeed, counting isomorphism classes of SL2(F q ′ ) is an easy task and we know that their number coincides with the number of isomorphism classes of irreducible representations so it suffices to check that the representations above are mutually inequivalent which is an elementary task. This explicit description first appears in the paper [START_REF] Brauer | On the modular character of groups[END_REF] of Brauer and Nesbitt. Steinberg tensor product theorem [START_REF] Malle | Linear algebraic groups and finite groups of Lie type[END_REF]Theorem 16.12] provides such a description when, at the place of G = SL2, we have, much more generally, a semisimple algebraic group of simply connected type, defined over an algebraically closed field B of positive characteristic. This also implies Lemma 8. The author is thankful to Gebhard Böckle for having drawn his attention to this result and reference.

Some representations of GL2(A)

. We now set q = p e with e > 0. We also set K := Fq(t) for a variable t all along this subsection. We consider the algebra homomorphism χt :

A → Fq[t] ⊂ K defined by χt(a) = a(t) = a0 + a1t + • • • + a d t d for a = a0 + a1θ + • • • + a d θ d ∈ A,
with coefficients ai ∈ Fq. We extend our notations by setting, for a matrix M with entries in A, χt(M ) the matrix obtained applying χt entry-wise. We denote by ρt, ρ t,l , ρ I t,l the representations χt • ρ1, χt • ρ l , χt • ρ I l over K-vector spaces with the appropriate dimensions, of the group Γ = GL2(A).

Lemma 10. For all l as above, the representation ρ I t,l is irreducible. Proof. It suffices to show that the restriction to SL2(Fp[θ]) ⊂ Γ is irreducible. Let us consider an element ζ ∈ F ac q of degree f and let us denote by F q ′ with q ′ = p f the subfield Fp(ζ) of F ac p . The group homomorphism ev ζ : SL2(Fp[θ]) → GL2(F q ′ ) defined by the entry-wise evaluation ev ζ of θ by ζ has image SL2(F q ′ ). Indeed, the evaluation map ev ζ : Fp[θ] → F q ′ is surjective, the image of SL2(Fp[θ]) by ev ζ clearly contains the subgroup of triangular upper and lower matrices with coefficients in F q ′ , which are known to generate SL2(F q ′ ) We set N = φp(l). Let V be a non-zero K-subvector space of K N which is stable under the action of the representation of SL2(Fp[θ]) induced by ρ I t,l . Let us fix a basis b of V . We choose f big enough so that q ′ > l, q and the image b ′ of b in F N q ′ by the evaluation at t = ζ is well defined and non-zero. Then, the F q ′ -span of b ′ is a non-trivial sub-vector space of F N q ′ which is left invariant under the action of ρ l , which is impossible.

Remark 11. Let m be a class of Z/(q -1)Z and let us consider the representation ρ I t,l,m : Γ → GL φp(l) (K) defined by ρ I t,l,m := ρ I t,l ⊗ det -m . By Lemma 10, it is irreducible. However, the representations ρ I t,l,m do not cover all the irreducible representations of Γ in GLN (K) for some N . Due to the fact that we evaluate the functor GLN on a ring which is not a field (here, the ring A), there are irreducible representations which, after specialization at roots of unity, do not give irreducible representations of SL2(F q ′ ).

Remark 12. The group S (p) of p-adic digit permutations of Zp discussed by Goss in [START_REF] Goss | ζ-phenomenology[END_REF] acts on the positive integers l by means of their expansions in base p. This defines an action of the group S (p) on the set of representations ρ I l by ν(ρ I l ) = ρ I ν(l) , for ν ∈ S (p) . Note that the dimensions of these representations are S (p) -invariants. It is easy to show that ν(ρ I l ) ∼ = ρ I l ′ if and only if ν(l) = l ′ . Remark 13. We are thankful to Pietro Corvaja for having pointed out the following property. Let k be a perfect field. Then, for all γ ∈ SL2(k ac ) there exists a morphism φ : A 1 → SL2 defined over k and α ∈ k ac , such that φ(α) = γ.

Products of representations

Let t1, . . . , ts be independent variables. We denote by t s the set of variables (t1, . . . , ts) and we set Ks = Fq(t s ). If s = 1, we write t = t1 and we have Ks = K, the field of §3.2. We also consider l = (l1, . . . , ls) an s-tuple with entries in Z which are ≥ 1.

Theorem 14. the representation

ρ II t,l := ρ I t 1 ,l 1 ⊗ • • • ⊗ ρ I ts,ls : Γ → GL φp(l 1 )•••φp(ls) (Ks) is irreducible.
Proof. We set N = φp(l1) • • • φp(ls). Let us suppose by contradiction that the statement is false. Then, there exists a Ks-sub-vector space V = {0} ⊂ K N s such that for all γ ∈ Γ, ρ II t,l (γ)(V ) ⊂ V . Let us fix a basis v = (v1, . . . , vr) of V . For integers 0 ≤ k1 ≤ • • • ≤ ks, we denote by ev the map Fq[t s ] → Fq[t] which sends a(t1, . . . , ts) ∈ Fq[t s ] to a(t k 1 , . . . , t ks ) ∈ Fq[t]. This map is a ring homomorphism whose kernel is the prime ideal P generated by the polynomials tj -t q k j -k j-1 j-1 , j = 2, . . . , s. We consider the associated multiplicative set S = Fq[t s ] \ P. Then, the evaluation map ev extends to S -1 Fq[t s ] which is Zariski dense in Ks = Fq(t s ). We now extend ev coefficient-wise on every matrix, vector, etc. with entries in S -1 Fq[t s ]. If k1 is big enough, ev(v) is well defined and non-zero.

We can in fact choose k1, . . . , ks so that we also have at once, ev(ρ II t,l ) = ρ I t,l for some l ≥ 0. Indeed, if we write the p-expansions li = li,0 + li,1p + • • • + li,rp r (i = 1, . . . , s) for some r ≥ 0, then we can choose k1, . . . , ks so that there is no carry over in the p-expansion of the sum l = l1q k 1 + l2q k 2 + • • • + lsq ks ; for such a choice of k1, . . . , ks, ev(ρ II t,l ) is thus irreducible. We now set W to be the K-span of ev(v), well defined and non-trivial in K N (we recall that K = Fq(t)). Let w be in W . We can write w = a1 ev(v1) + • • • + ar ev(vr) for elements ai ∈ K. Then,

ρ I t,l (γ)(w) = a1ρ I t,l (γ)(ev(v1)) + • • • + arρ I t,l (γ)(ev(vr)) = a1 ev(ρ II t,l (γ)(v1)) + • • • + ar ev(ρ II t,l (γ)(vr)
) is a vector of W , hence contradicting the irreducibility of ρ I t,l .

Applications to Poincaré series

Definition 15. We say that a representation Γ ρ -→ GLN (K) is normal to the depth L ∈ {1, . . . , N } if for all γ ∈ H = {( * * 0 1 )} ⊂ Γ, we have that ρ(γ) = ( * * 0 I L ), where IL denotes the identity matrix of size L. A representation as above which is normal to the depth N has finite image. To see this, note that ρ((

* * 0 * )) = (( * 0 0 * )) is finite. Hence, ρ * 0 * * = ρ 0 1 1 0 * * 0 * 0 1 1 0 = = ρ 0 1 1 0 ρ * * 0 * ρ 0 1 1 0 = ρ 0 1 1 0 ρ * 0 0 * ρ 0 1 1 0 = ρ 0 1 1 0 * 0 0 * 0 1 1 0 = ρ * 0 0 * .
We thus have ρ( * 0 * * ) = ρ( * * 0 * ) finite, and

ρ(Γ) = ρ(( * * 0 * )( * 0 * * )) = ρ( * 0 0 * ) is finite. The representation Γ ρσ --→ GLN (K) with N = 2d associated to an algebra representation A σ -→ Mat d×d (K) is normal to the depth L = d.
If, for some ring R, we have that M ∈ MatN×N (R) = ( * * X Y ) with Y ∈ MatL×L, we set ML = (X, Y ) ∈ MatL×N (R). In other words, ML is the matrix constituted by the last L lines of M .

We denote by Ω = C∞ \ K∞ the Drinfeld "upper-half plane" of C∞. We choose m a non-negative integer, an integer w ∈ Z>0, and, for δ ∈ Γ and z ∈ Ω, we set µw,m(δ, z) = det(δ) -m J δ (z) w , where Jγ (z) is the usual "Drinfeldian" factor of automorphy defined, for γ = ( a b c d ) ∈ Γ by Jγ (z) = cz + d. We also denote by u(z) the uniformizer at infinity of Ω, that is, the function u(z) = 1 e C (z) with eC the exponential function C∞ → C∞ with lattice period A ⊂ C∞.

We consider a representation Γ Ew,m,ρ : Ω → MatL×N (K), in the sense of [START_REF] Pellarin | On certain generating functions in positive characteristic[END_REF].

Remark 16. For convenience of the reader, we recall here the definition of an holomorphic function Ω → K. For z ∈ Ω, we set |z| ℑ := inf λ∈K∞ |z -λ|, which is non-zero. We also define, on Ω, a Stein-like structure by considering the affinoids Un = {z ∈ Ω; |z| ≤ q n and |z| ℑ ≥ q -n }, so that Ω = ∪ n∈N Un. For n fixed, a function f : Un → K is holomorphic if it is a uniform limit of a converging sequence of rational functions Un → K, without poles in Un. A function f : Ω → K is holomorphic if, for all n ≥ 0, the restriction of f to Un is holomorphic.

Following and readapting the proof of [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF]Proposition 22], we obtain: Proposition 17. The following properties hold, for w ∈ Z>0, m ∈ Z ≥0 and ρ a representation Γ → GLN (K):

(1) For all γ ∈ Γ, we have

Ew,m,ρ(γ(z)) = det(γ) -m Jγ (z) w Ew,m,ρ(z) • ρ(γ) -1 , (2)
There exists h ∈ Z such that

u(z) h Ew,m,ρ(z) → 0 ∈ MatL×N (K)
as u(z) → 0.

The last condition means that Ew,m,ρ(z) is tempered in the sense of [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF]. The proposition means that the L columns of the transposed of Ew,m,ρ are vectorial modular forms of weight w and type m with respect to the contragredient representation of ρ. In the next two subsections, we analyze Poincaré series associated with two particular classes of representations. (1) If w -1 ≡ 2m (mod q -1), then Ew,m,ρ = 0, identically.

(2) If w -1 ≡ 2m (mod q -1) and w ≥ (q + 1)m + 1, then, the rank of the matrix function Ew,m,ρ = 0 is d. (3) In the second case, each row of the matrix function Ew,m,ρ has the entries which are K-linearly independent.

Proof. The hypotheses on σ imply that the matrix ϑ = σ(θ) has distinct conjugate eigenvalues λ1, . . . , λ d ∈ K ac none of which lies in F ac q . We consider a corresponding basis v1, . . . , v d ∈ (K ac ) d of eigenvectors (considered as column matrices) which are then common eigenvectors for all the elements of the image of σ. In (K ac ) 2d = (K ac ) N we consider the basis w1, . . . , w 2d defined by wi = vi ⊕ 0 and w d+i = 0 ⊕ vi for i = 1, . . . , d. We also denote by M ∈ GLN (K ac ) the matrix whose columns are the wi's for i = 1, . . . , 2d. then, for δ = ( a b c d ) ∈ Γ, we have

ρ(δ)LM = δ(t) * (v1, . . . , v d ) := (c(λ1)v1, . . . , c(λ d )v d , d(λ1)v1, . . . , d(λ d )v d ) ∈ Mat d×2d (K 2d ).
Hence we have, with the same significance of the product * extended linearly, that

M • Ew,m,ρ = Ew,m,χ t * (v1, . . . , v d ),
where Ew,m,χ t : Ω → Mat1×2(K) is the function defined by

Ew,m,χ t (z) = δ=( a b c d )∈H\Γ µw,m(δ, z) -1 u m (δ(z))(c(t), d(t)).
This matrix function is the deformation of vectorial Poincaré series Ew,m(z, t) considered in [7, Proposition 22] and we know the following:

• If w -1 ≡ 2m (mod q -1), then Ew,m,χ t is identically zero.

• If w -1 ≡ 2m (mod q -1) and w ≥ (q + 1)m + 1, then all the entries of Ew,m,χ t are non-zero.

We now observe that if C is a complete field containing A and if

f (t) = i≥0 fit i ∈ C[[t]
] is a non-zero formal power series, with fi → 0 for i → ∞ (an element of the Tate algebra of formal series with coefficients in C in the variable t) then, for λ ∈ K ac \ F ac q , we have that f (λ) = i≥0 fiλ i converges in the complete field K ♯ := Frac(C ⊗ Fq K ac ) (with K ac carrying the trivial norm) to a non-zero element.

Since M is invertible, Ew,m,ρ is identically zero if and only if Ew,m,χ t is identically zero (we have supposed that ϑ has no eigenvalues in F ac q ) and in the case of non-vanishing, the rank is maximal equal to d. Properties 1) and 2) of our proposition hence follow from Proposition 22 of [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF].

It remains to show the part 3); this follows from Lemma 7. Indeed, assuming that w-1 ≡ 2m (mod q-1) and w ≥ (q + 1)m + 1, let i be an index between 1 and d; we know that it is non-zero. Let us assume, by contradiction, that the entries of E are linearly dependent; then, the vector space V whose elements are the vectors v ∈ (K ♯ ) N such that E (z) • v = 0 for all z ∈ Ω, is non-trivial.

Let v be in V . For all γ ∈ Γ, we have

0 = E (γ(z)) • v = det(γ) -m Jγ (z) w E (z) • ρ(γ) -1 • v.
This means that ρ(γ) -1 • v ∈ V so that ρ(γ)(V ) ⊂ V for all γ ∈ Γ. Since ρ is irreducible, we thus have that V = (K ♯ ) N but E is non-zero, whence a contradiction.

5.2.

Vectorial Poincaré series associated to the representations ρ II t,l . We now consider the settings of §4 and we return to independent variables t s and to the field Ks = Fq(t s ). We also consider l = (l1, . . . , ls) an s-tuple with entries in Z which are ≥ 1 and we note that the representation ρ = ρ II t,l of Theorem 14 is normal to the depth L = 1.

Proposition 19. We have the following properties, for w > 0 and m ≥ 0, and with ρ the above considered representation.

(1) The function Ew,m,ρ : Ω → Mat1×N (K),

Other representations of Γ

Let K be a field containing a fixed base field k of positive characteristic (e.g. k = Fq) and let us consider a group representation ρ : G → GLN (K). The essential dimension (over k) of ρ is the transcendence degree over k of the field generated by the entries of the image of ρ. If G is finite, then the essential dimension of ρ is zero. In this paper, we have studied several examples in the case k = Fq and G = Γ. For instance, the essential dimension of the tautological representation Γ → GL2(A) is one, and the essential dimension of a representation ρ II t,l as in Theorem 14 is s, the number of variables in t s . As a conclusion of the present note, we would like to point out that there are irreducible, finite dimensional representations of GL2(k[t]) with infinite essential dimension. Indeed, for any field k, a Theorem of Nagao (see [START_REF] Nagao | On GL(2, K[x[END_REF]Theorem 2] and Serre, [9, II.1.6]) asserts that Remark 23. The group SL2(Z) has uncountably many isomorphism classes of irreducible complex representations and their explicit classification is not yet understood. A similar question arises with the group GL2(A) and its representations in a complete algebraically closed field of characteristic p. The complete classification for SL2(Z) is however accessible if we impose an upper bound on the dimension. In [START_REF] Tuba | Representations of the braid group B3 and of SL(2, Z)[END_REF], Tuba and Wenzl obtained a complete classification of irreducible representations of the braid group B3 of dimension ≤ 5 yelding a similar result for irreducible complex representations of SL2(Z); it turns out that these families algebraically depend on finitely many parameters (eigenvalues, characters etc.). It would be nice to have a similar result for GL2(A).

Lemma 5 .

 5 and the series converges in the completion of K[x1, . . . , xs] for the Gauss norm extending | • |. We have the formula det(Lσ(n)) = Ls(n) x j =λ i,j j=1,...,s ∈ Ks,∞.

  ρσ --→ Mat 2d×2d (K), defined by ρσ a b c d = σ(a) σ(b) σ(c) σ(d) .

ρ-→

  GLN (K), normal to the depth L. Following [7, §2.4], we set, for δ ∈ Γ,f δ = µw,m(δ, z) -1 u m (δ(z))ρ(δ)L : Ω → MatL×N (K), where we recall that K = K1 is the completion of C∞(t) for the Gauss norm. It is easy to show that the series Ew,m,ρ(z) = δ∈H\Γ f δ , the sum being over the representatives of the cosets of Γ modulo the left action of H = {( * * 0 1 )}, converges to a holomorphic function

5. 1 .

 1 Vectorial Poincaré series associated to representations ρσ. Let us consider an irreducible, faithful algebra representation A σ -→ Mat d×d (K), and the associated representation Γ ρσ --→ GLN (K) with N = 2d, which is normal to the depth L = d. We additionally suppose that the characteristic polynomial of ϑ = σ(θ), irreducible, is also separable. Proposition 18. The following properties hold, with ρ = ρσ.

( 2 )

 2 GL2(k[t]) ∼ = GL2(k) * B(k) B(k[t]),where, for a commutative ring R, B(R) denotes the group of upper triangular matrices with entries in R with invertible determinant and where * B(k) stands for the amalgamated product along B(k). Therefore, we have the following: Proposition 22. Any automorphism φ of GL2(k) extends to a group isomorphism between GL2(k[t]) and the subgroup Φ ∞ of GL2(k[x1, x2, . . .]) generated by GL2(k) and the matrices λ x i 0 µ , where x1, x2, . . . are independent indeterminates over k and λ, µ ∈ k × . Proof. By (2), we see that the association λ t i 0 µ → λ x i 0 µ extends to give the above group isomorphism.The above proposition exhibits representations GL2(k[t]) → GL2(K∞) where K∞ = k(x1, x2, . . .), which have infinite essential dimension over Fq.

Acknowledgement. The author thanks Gebhard Böckle, Mihran Papikian and the Referee, for useful hints and remarks that have contributed to improve and correct the paper.

This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme under the Grant Agreement No 648132.

with N = φp(l1) • • • φp(ls) is well defined, holomorphic, tempered, and satisfies Ew,m,ρ(γ(z)) = det(γ) -m Jγ (z) w Ew,m,ρ(z) • ρ(γ) -1 , γ ∈ Γ.

(2) If w ′ := w -l1 -• • • -ls ≡ 2m + 1 (mod q -1), then Ew,m,ρ ≡ 0.

(3) With w ′ defined as above, if w ′ ≡ 2m + 1 and w ′ ≥ (q + 1)m + 1, then Ew,m,ρ = 0. (4) If m = 0 and w ′ ≡ 1 (mod q -1), then Ew,m,ρ = 0.

(5) In all cases in which Ew,m,ρ = 0, its entries are linearly independent over K.

Proof. The first two properties and the last one are simple variants of the corresponding parts of Proposition 18. For the third property, we consider the matrix function

1 and where we have used the expansions in base p of l1, . . . , ls: li = li,0 + li,1p + • • • + li,r i p r i with ri = 0 for i = 1, . . . , s. Then, as in [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF], we note that

the Poincaré series of weight w ′ and type m so that we can conclude with [4, Proposition 10.5.2]. The property 3) is not enough to show the property 4), but we can proceed more directly by noticing that in this case,

Hence, if we suppose that u(z) → ∞, then Ew,0,ρ → (0, . . . , 0, 1).

The transposed of the matrix functions Ew,m,ρ are thus vectorial modular forms of weight w, type m associated to the representations t ρ in the sense of [START_REF] Pellarin | Values of certain L-series in positive characteristic[END_REF]. (the dash ′ denotes a sum which avoids the couple (0, 0)). This defines a holomorphic function

Let, on the other side, ρ be the representation ρ : Γ → Mat 2d s ×2d s (K) defined by ρ = ρσ 1 ⊗ • • • ⊗ ρσ s . The following lemma is easy to verify.

Lemma 20. We have the identity Gw,σ = Lσ(w)Ew,0,ρ.

The matrix Lσ(w) is the L-value associated to the semi-character σ as defined in §2.2.2. This and Proposition 6 suggest that the Eisenstein series Gw,σ could be also related to Taelman units. Of course, this is quite speculative, because at the moment, we do not have at our disposal any kind of metric over the spaces of vectorial modular forms that we consider, allowing us to define an appropriate notion of unit group of Taelman in this setting. However, this seems to suggest the following conjecture.