dataesr/scientific-paragraphs-categorization huggingface dataset:
Leakage Preservation The first case we consider is one where leakages are preserved by compilation. This case is actually the one covered by compiler correctness and can thus leverage directly the many already existing lemmas and theorems of CompCert. It is directly stated and proved on the instrumented semantics →. Theorem 5. 2 (Constant-time security preservation by leakage preservation). Let S be a safe source program and T be the target compiled program. If S is constant-time w. r. t. φ then T is constant-time w. r. t. φ, provided that the relation ≈ between program states is a trace preserving simulation (w. r. t. →) as defined in Figure  2. Proof. First we observe that such simulation implies that the leak-only semantics satisfies a leak-preserving simulation. This simulation is the classic forward simulation used in CompCert   1 ), including passes that do not optimize conditional branches, nor memory accesses.
These passes are then especially easy to adapt to constant-time preservation since we can reuse the same proof script as for the original simulation proof. This is a great time saver for a pass like RTLgen (which transforms a structured Cminor program into a RTL control-flow graph) because its soundness proof is quite verbose. However, many optimizations do not preserve leakages. Indeed, optimizations such as common subexpression elimination (CSE) or constant propagation can remove memory accesses or even branchings if they manage to conclude that a condition always evaluates to the same truth value.
The following theorem states that constant-time security is preserved by a leakage-erasing simulation. Its proof is postponed at the end of Section 5. 5. Theorem 5. 7 (CTS preservation from leakage-erasing simulation). Let S be a safe source program and T be the target compiled program. If S is constant-time w. r. t. φ then T is constant-time w. r. t. φ, provided that ≈ n is a leakage-erasing simulation and is same-point congruent. Because the definition of leakage-erasing simulation is very close to the standard CompCert trace-preservation diagram, we were able to pleasantly reuse most of the existing proof scripts. For each simulation, the original proof starts with a case study on the current source instruction; if the instruction preserves the trace we reuse the same script, otherwise we prove that it erases all the leakages, which is generally an easy proof task and concerns very few instructions.
On the other hand, it may be quite difficult to write out the prediction for the number of steps taken by the target state when the corresponding source state takes one step. The process is however proof driven as this index is already embedded in the proof in CompCert. It is then needed to understand the proof details, which can be quite involved. For instance, the proof script for the Cminorgen pass uses dependent inductions within the main induction on the source steps. This indicates what the predicted number of steps depends on. In such a case of a recursive simulation, the index depends on the proof depth. This simulation is satisfied by many CompCert passes (5 among 17, see Table  1 ). Still, there remain passes that require more advanced reasoning. We describe them in the upcoming subsections.
CT-simulation with a Cube Diagram Previous methods allow intensive reuse of existing CompCert proof scripts because they slightly strengthen classical simulation diagrams. In last resort, we rely on a full-fledged CT-simulation. For this purpose, we adapt the CT-simulation from  [Barthe et al. 2018 ] under our strengthened notion of same-point relation and its related properties. It is directly phrased using the leak-only semantics -→ l , but we omit the subscript. A CT-simulation can be split into two parts, namely a counting simulation and a CT-diagram. These are defined as follows. We consider a general notion of simulation relation ≈ n,h parameterized by a step-number prediction n and a history h. The exact nature of histories is kept abstract here. It can be instantiated with memory injections or more compound structures (for the inlining and assembly generation passes).
2012]  and mbedTLS  [ARM 2016 ]. These are C implementations that we experiment with in order to evaluate our compiler, but it should be reminded that if performance is an issue, it is generally better to use hand-optimized assembly code at the cost of portability. We first measured the execution times (using an Intel i7-8550U CPU 1. 8GHz, with 16GB of RAM), which are shown in Figure  10. We compiled these programs using the original CompCert, our version of CompCert, and gcc at different levels of optimization. As all programs have a very short execution time, we executed them from 10 6 to 10 9 times depending on the program. We obtain shorter execution times than gcc without optimization. This is a promising result, as cautious users who are wary of too aggressive compiler optimizations breaking constant-time security would use it to compile cryptographic implementations.
Limitations Among the 20 compiler passes of CompCert shown in Figure  11 , only 17 are present in Table  1. The first compiler pass from CompCertC to Clight is a determinization pass; it is removed as explained earlier (see Section 5. 1). Moreover, we encountered difficulties while doing the proofs and had to consequently make compromises: two passes were not proved to be security preserving, namely, SimplLocals and Unusedglob. They are still proved semantics preserving as in the original CompCert. SimplLocals is the second compiler pass. It pulls local scalar variables out of memory. C-like languages such as Clight are split into expressions and statements. Expressions include variable lookups (pointer dereferencing) and are modeled as memory loads under the hood; they must thus produce leakages as instructed by our leakage model.
However, expressions may contain multiple nested variable lookups and may thus produce multiple leakages. Modifying CompCert so that the evaluation of expressions may generate leakages is a large endeavour. We therefore chose instead to normalize the source code so that memory loads can only be found at right hand sides of assignments (e. g. , the code f( * x + * y); becomes t1 = * x; t2 = * y; f(t1 + t2);). This standard transformation is commonly used to facilitate analyses (e. g. , the Verasco  [Jourdan et al. 2015]  and VST  [Appel 2011 ] tools use it). Unfortunately, normalizing code before the SimplLocals pass results in significant performance reduction. We hence compromised by performing the normalization after the SimplLocals pass, and prove security preservation starting after the normalization.
2019 ] is cast as typepreserving compilation. Unlike our work which targets an end-to-end compiler, these works focus on selected parts of the compilation chain. Our work is concerned about preservation of constant-time. However, it is also critical to verify that constant-time is enforced properly in the first place. To this end, several authors have developed fully automated methods. In unpublished work, Langley  [Langley 2010 ] developed a variant of Valgrind to verify that implementations are constant-time. A formally verified type-based analysis for constant-time security of CompCert assembly was proposed in  [Barthe et al. 2014 ]. The analysis relied on a simple alias analysis, which limited its applicability. Later, a more powerful analysis based on the Verasco analyzer was implemented for the Csharpminor intermediate language of CompCert  [Blazy et al.
2019 ]. The analysis could handle more examples than  [Barthe et al. 2014]  but was not verified formally. A more powerful type-based static analysis for LLVM programs is proposed in  [Rodrigues et al. 2016 ] and used to verify a large body of cryptographic algorithms. Independently, a sound and (relatively) complete approach based on product programs has been proposed also for LLVM, and also used to analyze large code bases. More recently, a variant of this approach based on relational Hoare logics has been used for proving constant-time security of Jasmin programs  [Almeida et al. 2019]. Further work considers constant-time security of floating point operations  [Andrysco et al. 2015 [Andrysco et al. , 2018] ]  and hardware implementations  [von Gleissenthall et al. 2019]. Formal Verification of a Constant-Time Preserving C Compiler 7:27 In a different direction, several works have used the CompCert compiler to produce formally verified cryptographic libraries.
For instance,  Appel et al. [Appel 2015; Beringer et al. 2015; Ye et al. 2017 ] use the Verified Software Toolchain  [Appel 2014 ] to prove functional correctness of cryptographic implementations, and the CompCert compiler to carry these guarantees to assembly code. Similarly, Zinzindohoué et al. [Zinzindohoué et al. 2017 ] use CompCert to generate assembly from HACL* implementations. These works assume that CompCert preserves constant-time; it would thus seem very beneficial to use our modified compiler to prove that the generated assembly code is indeed constant-time.
ACKNOWLEDGMENTS This work is supported by  DFF  project  6108-00363  from The  Danish Council for Independent Research for the Natural Sciences (FNU) ; by the  Office of Naval Research  under projects  N00014-12-1-0914 ,  N00014-15-1-2750  and  N00014-19-1-2292 ; and by a  European Research Council (ERC)   Consolidator Grant  for the project łVESTAž, funded under the European Union's  Horizon 2020 Framework Programme  (grant agreement no. 772568 ). The selection operation presented in Section 4. 2. 1 was discussed with Xavier Leroy who integrated it into CompCert version 3. 6.
Grain-legume crops are important for ensuring the sustainability of agrofood systems. Among them, pulse production is subject to strong lock-in compared to soya, the leading worldwide crop. To unlock the situation and foster more grain-legume crop diversity, scientific research is essential for providing new knowledge that may lead to new development. Our study aimed to evaluate whether research activity on grain-legumes is also locked in favor of soya. Considering more than 80 names grouped into 19 main grain-legume species, we built a dataset of 107,823 scholarly publications (articles, book, and book chapters) between 1980 and 2018 retrieved from the Web of Science (Clarivate Analytics) reflecting the research activity on grain-legumes. We delineated 10 scientific themes of interest running the gamut of agrofood research (e.
Consequently, the number of bibliometric analyses has been growing for a variety of fields: in electronics  [23] , on scientific parks and the links to open innovation  [24] , or in pharmaceuticals  [17]. However, few have been done in agriculture (e. g. , on agroecology  [25] ), even though there are key sustainability issues challenging research. To evaluate the respective shares of grain-legume species in the sciences, we used the Web of Science (WoS) collection to retrieve the scholarly publications reflecting research activity recognized by peers. As advanced by STS, and more specifically by scientometrics studies  [19] , these research papers remain the highest quality variable to reflect research activity on a given topic. Even though GS (Google Scholar) is growing and presented as alternative, the metadata offered by GS are still very limited, reducing the practical suitability of this source for large-scale citation analyses.
In addition, GS includes around 20-50% of other type of research documents (depending on the scientific fields), such as PhD dissertations, scientific reports, and non-peer-reviewed papers that create bias in comparing research advancement from more qualitative types of research documents  [26]. Moreover, language harmonization rules are required to collect data on GS. Therefore, although perhaps not a perfect resource to reflect all the scientific knowledge stock, we chose a traditional bibliometric platform, as the WoS as better for providing more a relevant overview of peer-reviewed research activity (i. e. , the scholarly documents such as articles in peer-reviewed journals, books and book chapters), 97% of which were written in English on the WoS. An alternative bibliometric platform is Scopus, but we chose WoS thanks to our institution access; and Scopus use will generate additional computing methods to extract large collection as we did on the WoS, without adding so much other records as WoS and Scopus present high overlap level  [26].
This original and ambitious literature review involved 26 scientific experts on legumes, coupled with database and scientometrics experts to create relevant search queries on the WoS and appropriate software to process and analyze the resulting bibliographic records. Our findings are based on a core corpus totaling 107,823 scientific publications (i. e. , records) retrieved by thematic search queries addressing the title, abstract, and authors' keywords. Since soya is a major crop used for oil unlike most other grain-legumes, we excluded records referring to the subject of "soya oil", in order to have more relevant comparisons in the corpus created. Our results show that soya is mentioned in 43% of the records, groundnut in nearly 10% and all other pulses combined in 47%. The analyses revealed a strong imbalance within grain-legume species research, with soya dominant over all other grain-legume species; and if "soya oil" had been included in keyword searches, this percentage would be even greater.
Overview of the Methodology Adopted This study was based on a bibliometric dataset retrieved from the Web of Science (WoS) a product of Clarivate Analytics. As mentioned in Section 1, Scopus is the other prominent bibliographic database, which presents a high overlap with the WoS: see  [26]  for a comparison of these databases stressing their limitations and advantages to conduct large-scale literature analyses. The WoS is one of the most used bibliometric resources in the world. It provides access to article records from more than 30,000 journals and books in various fields of science. The WoS "Core Collection" includes about 70 million records  [27]. For the present study, we worked with several scientific experts to identify domain-specific keywords and retrieve the associated scientific publications (records).
First, we identified keywords covering most of the cultivated grain-legume species in Western countries (Species query). Second, we determined 10 domain-specific themes covering the main research issues on grain-legumes (e. g. , Allergy). Then, search queries on the WoS were designed to delineate the species and each theme (Table  1 ), leading to 10 thematic corpora on grain-legumes. Finally, these 10 corpora were merged into a single corpus called Fusion. All search queries and the associated publication records are available as open data from the https://data. inra. fr repository (Appendix A, Table  A2 ). In this article, a "corpus" is a set of records retrieved from the WoS and a "record" refers to the metadata of a scholarly document (e. g. , the type of publication, such as "article", "book chapter"; the authors; etc.
Theme experts We identified leading scientists in several fields (Table  1 ) who helped to delineate search queries for 10 key themes and to check the validity of the records retrieved. (Delineation of scientific fields or subject areas is a question under much discussion in scientometrics. Bibliometric databases developed their own classification reflecting the scope of journals. As such classification were not directly suitable to break down agricultural and food research activity in several fields on which to build our search queries, we relied on experts' judgement to define 10 themes of main interest covering the research on grain-legumes. We used the term of "theme" as a synonym of "subject area". See  [20]  to go further on this question of delineation of scientific fields).
• Scientometricians We collaborated with scientists who specialize in the quantitative study of science and database management systems to create an online platform giving access to the corpora collected. This platform was used to then incrementally refine search queries to build the corpora. Since the number of records to collect from the WoS (100 k) exceeded the amount of records one can extract from the web interface (limited to 5 k), we resorted to a Web of Science Data Integration feature. Data collection was then performed with an in-house program using the Web of Science API Expanded. Regarding the 10 domain-specific themes selected, we adopted a broad-spectrum approach covering the end-to-end workflow of grain-legume research from production to consumers. A growing concern in Western countries is to increase legume consumption  [28] ; therefore, we made sure to cover allergy and consumer acceptance subjects.
Indexing as a Post-Processing Step to Cleanse the WoS Results WoS queries were issued with the standard TS operator, meaning Topic Search. TS results collect records of the database that match the user's query on the following criteria: title, abstract, author keywords, and KeyWords Plus. KeyWords Plus are additional terms automatically generated by the WoS and attached to the records. Terms appearing more than once in the titles of the cited references in a record (i. e. , in its bibliography section) are called KeyWords Plus  [29]. For instance, a search like TS = "protein AND pea" matches documents whose title, abstract or author's keywords contain the term "protein" but not "pea", because the term "pea" occurred only in the bibliography of the document retrieved ("pea" being a KeyWords Plus here) (see, for instance, query UT = "WOS:000226807600008" AND TS = ("protein" AND "pea") yielding one journal paper on rice mutants, whose abstract contains "protein" but not "pea").
• Checking of the entire thematic corpus. This second task relied on descriptive statistics. For each thematic corpus, experts were instructed to assess the relevance of the most frequent: terms in the title, abstract, authors' keywords of the records; and WoS categories (wcs) reflecting the scope of the journal or the book that the WoS attributes to each record of the bibliographic database. Irrelevant terms or wcs with high frequencies relative to the thematic corpora were identified and used to adapt, once again, the search query. In particular, this led the experts to specify excluding conditions (see below). During this phase, the experts of closely related scientific themes (for instance, between Ecophysiology and Agronomy, or between Nutrition and Processing) collaborated to better delineate each theme.
Focus on the Design of the Species WoS Query The 10 thematic search queries were combined with a query targeting the names of grain-legume species. Hence, delineating the various terms referring to grain-legumes was a crucial part of our bibliometric study. This was a challenging task as different names are used in different scientific fields. Either the scientific name (generally the Latin name) or various, country-specific, common names were used. The expertise of two senior researchers internationally recognized on those crops, combined with the consulting of websites dedicated to data collection on plants (Table  2 ) and books This figure summarizes the main steps followed to build the thematic corpora. First, queries were submitted to the Web of Science to collect bibliographic records for each theme (Steps 1.
Results and Discussion Bibliometric analysis allowed us to mine this dataset and infer new knowledge on grain-legume research at the global scale. The main purpose of this paper is to shed light on the share of species in these corpora, reflecting the research activity on grain-legumes. Thus, we calculated the percentage of records on each species within the corpora, longitudinally and at different levels of analysis, according to species, themes, and countries, especially by comparing soya and pulse frequencies. Then, we discuss the implication of these results as regards avenues for future research and policies regarding the question of crop diversity.
Conclusions Understanding the dynamics of research is an epistemic project that concerns all sciences and is one primary focus of STS. Analyzing bibliometric datasets help both decision-makers for science policies and scholars to orient science and, in the end, innovation. By using scientometric indicators on the metadata of scholarly documents retrieved from the WoS, we gave an overview of the research output on grain-legumes since 1980 at the global scale. We quantified the shares of species, analyzed by main academic fields (i. e. , themes) and countries. To establish these results, this work developed a rigorous methodology for building a bibliometric dataset and a processing software, which can be used for further bibliometric research on other crops to bring a larger analysis of the dynamics of research activity on agricultural and food systems.
Given that we are faced with an ever increasing amount of published data, involving researchers on the measurement of sciences is essential. Moreover, those researchers could advise other researchers on the way to communicate about their work. Indeed, the way bibliometric datasets are collected and how researchers describe their works through the title, abstract, and keywords of records impact the ways we can analyze research patterns through bibliometric data. Title, abstract, and keywords are the main data on which scientometric studies relies, and thus their contents strongly determine the results obtained. Our findings raise another question about the way species are mentioned: a common dictionary of species names in scientific platforms, such as the WoS, would help to better follow species, and to conduct longitudinal analysis on the percentage of any crop in research and their links.
Thirdly, we used English-language scholarly publications, such as peer-reviewed articles, books, and book chapters, to reflect research activity and to give an overview of the majority of the scientific knowledge on grain-legumes. Other data collections could enrich our dataset to have a more complete overview. The first improvement will be to add records retrieved from the Scopus Collection (the other most used bibliometric platform), even though the WoS and Scopus overlap considerably for certain disciplines  [26]. This could lead to some adjustments in the shares of themes, but probably not in their ranking. Other enrichments such as using alternative search engines, e. g. , Google Scholar (GS), will require methodological solutions. GS provides access to larger collection of research such as PhD theses, scientific reports, and non-peer-reviewed articles, but no software exists to retrieve large collections from GS.
In addition, no rigorous metadata are associated to enable relevant analysis among the various documents once they are collected. Last, while English dominates scientific publications, other languages are still used and including them would complicate larger record harvesting and analyses from GS. "The second most frequent language of unique GS citations was Chinese (4-12%), and all other languages have a share of 4% or lower across all subject areas. A few (5-10%) unique GS citations were published in languages outside the top 11 most frequently used languages overall"  [26]  (p. 14). To have a better overview of the evolution of this scholarly scientific knowledge on grain-legumes, further studies can be done (based on this dataset or an enriched dataset) such as semantic or socio-semantic network analysis.