Diffusion afp-devel 72772a622eb3

merged
72772a622eb3
Actions

Tags

None

Subscribers

None

Description

merged

Details

Provenance

Authored on

Parents

rAFP11a3d3871dea: New entry CRYSTALS-Kyber
rAFPafc81491665d: regenerate site;

Branches

Unknown

Tags

Unknown

Event Timeline

paulson committed rAFP72772a622eb3: merged.Sep 8 2022, 5:44 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

afc81491665d regenerate site;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
791a909ac26e added missing history in metadata;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
ac2b59b37741 retrieve missing change history in metadata migration tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
490d1fdcd266 backout b2ae7c2c3ea51af8f43b76cdcb5d499c5085e726
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
17b82e6796f6 adapt to only check ROOT for directories in thys (aftermath of…
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9e2b85708f73 updated entry for Universal Turing Machines
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
da1092b22903 merged
Author
desharna
Browse Repository
No Builds
No Audits
13d7491c6ab9 adapted to antimono
Author
desharna
Browse Repository
No Builds
No Audits
12747ed77d71 merged
Author
desharna
Browse Repository
No Builds
No Audits
64d28014cec0 adapted to new mono and strict_mono
Author
desharna
Browse Repository
No Builds
No Audits
17f4fbb45f9c updated to Isabelle/5ea588440b06
Author
desharna
Browse Repository
No Builds
No Audits
ff719c05809a Updated citations
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
73f15452e56f Updated citations
Author
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
Browse Repository
No Builds
No Audits
6c87f24bb773 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
14eb275d680e merged
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
f294e5dddd66 Substantial additions by Franz Regensburger to the Universal_Turing_Machine…
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
5a1267ab6b71 tuned timeouts, based on test runs with threads=1;
Author
makarius
Browse Repository
No Builds
No Audits
10120a93e155 replaced slow smt call by blast
Author
blanchette
Browse Repository
No Builds
No Audits
337819a49c4b avoid hardwired document;
Author
makarius
Browse Repository
No Builds
No Audits
9839b66f7c66 merged
Author
paulson
Browse Repository
No Builds
No Audits
4ba03d4cf30e cosmetic
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ad3c436a878d replace smt_oracle by proper veriT reconstruction
Author
mathias.fleury
Browse Repository
No Builds
No Audits
15d285a97ae0 merged
Author
paulson
Browse Repository
No Builds
No Audits
a3d1b4509a4d tweaks
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
64cf94d5181c make all sessions of chapter "AFP" belong to group "AFP";
Author
makarius
Browse Repository
No Builds
No Audits
349b20f17308 chapter_definition for presentation;
Author
makarius
Browse Repository
No Builds
No Audits
edbde558808d Undo an unrelated change that somehow crept into the previous commit.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
13b9d5692b1e Remove lots of unnecessary explicit quantifiers in lemma statements, now that…
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
93b0051abb90 Revised locale structure and notation. Proposed modularization for ZF…
Author
sterraf
Browse Repository
No Builds
No Audits
358ee38a13a3 tuning
Author
blanchette
Browse Repository
No Builds
No Audits
13c41cab9c59 updated entries: Combinatorics_Words, Combinatorics_Words_Lyndon, and…
Author
Štěpán Starosta <stepan.starosta@fit.cvut.cz>
Browse Repository
No Builds
No Audits
f50360e11df7 avoid fact name clash
Author
florian.haftmann
Browse Repository
No Builds
No Audits
cf809a286330 adjusted to distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
939afa7484fc repaired proof
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d23129e35a65 Complex_Bounded_Operators: Fixed document generation
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
ec167025ccd6 Merged changes.
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
e7c507b5aeb1 Registers: Fixed parse error.
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
ee86e2d696c8 Misc updates to Complex_Bounded_Operators:
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
4c8bd587b4b0 Reintroduce type signatures.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
48b40c0c94af Switch to simultaneous substitutions.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
621bc6675749 merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
4b70dbdbeea7 merged
Author
makarius
Browse Repository
No Builds
No Audits
c8deb994f6e9 Isabelle/b6589c8ccadd officially supports README.thy;
Author
makarius
Browse Repository
No Builds
No Audits
59b0a80cf40b streamlined
Author
florian.haftmann
Browse Repository
No Builds
No Audits
26a20c98b97c tuned proofs
Author
florian.haftmann
Browse Repository
No Builds
No Audits
561d723d6358 discontinued obsolete README.html: superseded by abstract provided by AFP;
Author
makarius
Browse Repository
No Builds
No Audits
3d7eaa9f630e streamlined primitive definitions for integer division
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d186b2e87e18 tuned code equations for Xml-parsing
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
56991031ffef refactored algebraic number theories, generalized Cauchy Root Bounds lemma (so…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
fea99b2f42bf Revision of locale structure
Author
sterraf
Browse Repository
No Builds
No Audits

Changes (51)

Path

Size

CRYSTALS-Kyber.toml

Crypto_Scheme.thy

Crypto_Scheme_NTT.thy

Kyber_NTT_Values.thy

Kyber_Values.thy

Mod_Plus_Minus.thy

Mod_Ring_Numeral.thy

authors/

kreuzer/

data/

berlekamp_zassenhaus/

number_theoretic_transform

Berlekamp_Zassenhaus.html

CRYSTALS-Kyber.html

Number_Theoretic_Transform.html

statistics/

topics/

computer-science/

security/

rAFP72772a622eb3

metadata/entries/CRYSTALS-Kyber.toml

Loading...

thys/CRYSTALS-Kyber/Abs_Qr.thy

Loading...

thys/CRYSTALS-Kyber/Compress.thy

Loading...

thys/CRYSTALS-Kyber/Crypto_Scheme.thy

Loading...

thys/CRYSTALS-Kyber/Crypto_Scheme_NTT.thy

Loading...

thys/CRYSTALS-Kyber/Kyber_NTT_Values.thy

Loading...

thys/CRYSTALS-Kyber/Kyber_Values.thy

Loading...

thys/CRYSTALS-Kyber/Kyber_spec.thy

Loading...

thys/CRYSTALS-Kyber/Mod_Plus_Minus.thy

Loading...

thys/CRYSTALS-Kyber/Mod_Ring_Numeral.thy

Loading...

thys/CRYSTALS-Kyber/NTT_Scheme.thy

Loading...

thys/CRYSTALS-Kyber/Powers3844.thy

Loading...

thys/CRYSTALS-Kyber/ROOT

Loading...

thys/CRYSTALS-Kyber/document/root.bib

Loading...

thys/CRYSTALS-Kyber/document/root.tex

Loading...

thys/ROOTS

Loading...

web/authors/kreuzer/index.html

Loading...

web/authors/kreuzer/index.xml

Loading...

web/data/keywords.json

Loading...

web/dependencies/berlekamp_zassenhaus/index.html

Loading...

web/dependencies/berlekamp_zassenhaus/index.xml

Loading...

web/dependencies/index.html

Loading...

web/dependencies/index.json

Loading...

web/dependencies/number_theoretic_transform/index.html

Loading...

web/dependencies/number_theoretic_transform/index.xml

Loading...

web/entries/Berlekamp_Zassenhaus.html

Loading...

web/entries/CRYSTALS-Kyber.html

Loading...

web/entries/Number_Theoretic_Transform.html

Loading...

web/entries/index.html

Loading...

web/entries/index.xml

Loading...

web/index.html

Loading...

web/index.json

Loading...

web/index.xml

Loading...

web/sitemap.xml

Loading...

web/statistics/index.html

Loading...

web/theories/crystals-kyber/index.html

Loading...

web/theories/index.xml

Loading...

web/topics/computer-science/security/index.html

Loading...

web/topics/computer-science/security/index.xml

Loading...

web/topics/index.html

Loading...