Commits

Breadcrumbs

History for

onb388ce4

User selector

All users

Datepicker

All time

Commit History

Commits on Apr 5, 2024

• Made some initial changes to support OCaml version 5. This is mainly

  Show description for b388ce4
  jrh13

  committed
  b388ce4

Commits on Apr 4, 2024

• Abbreviate Num.num_of_int with num

  Show description for 3e016a4
  aqjune

  committed
  3e016a4

Commits on Apr 3, 2024

• Replace Int constructor with num_of_int

  Show description for 0262b9e
  aqjune

  committed
  0262b9e

Commits on Mar 20, 2024

• Added a basic bit-blasting tactic and rule to the word library, using

  Show description for c153f40
  jrh13

  committed
  c153f40

Commits on Mar 17, 2024

• Added a basic implementation of BDDs as a HOL derived rule, in the new

  Show description for 7e9faf7
  jrh13

  committed
  7e9faf7

Commits on Mar 2, 2024

• Added more word lemmas

  Show description for 44c12e0
  jrh13

  committed
  44c12e0

Commits on Feb 22, 2024

• Added some alternative definitions of Jacobian-coordinate elliptic

  Show description for 3d231f3
  jrh13

  committed
  3d231f3

Commits on Feb 19, 2024

• Add NAME_ASSUMS_TAC and PRINT_GOAL_TAC, improve error messages of a few decision procedures

  Show description for 36c005b
  aqjune

  committed
  36c005b

Commits on Feb 7, 2024

• Added just a few small lemmas, a couple abut machine words, and

  Show description for ea45176
  jrh13

  committed
  ea45176

Commits on Nov 3, 2023

• Added a construct "word_insert x (pos,len) y" which inserts a length len

  Show description for dcd765c
  jrh13

  committed
  dcd765c

Commits on Jul 21, 2023

• Enhanced INT_ARITH, INT_ARITH_TAC and ASM_INT_ARITH_TAC with better

  Show description for 29b3e11
  jrh13

  committed
  29b3e11

Commits on May 25, 2023

• Added an integer-scaled version of "divstep", which scales delta

  Show description for 40e6df2
  jrh13

  committed
  40e6df2

Commits on May 20, 2023

• Added quite a number of word-related theorems including a new

  Show description for 7a035fd
  jrh13

  committed
  7a035fd

Commits on Apr 26, 2023

• Add bm_check_disjointness

  Show description for 91d8a98
  aqjune

  committed
  91d8a98

• Added a formalization, with iteration bound proof from Dan Bernstein,

  Show description for 6f6ac17
  jrh13

  committed
  6f6ac17

Commits on Apr 15, 2023

• Made a few additional enhancements and cleanups to WORD_BLAST, in particular

  Show description for 6835b31
  jrh13

  committed
  6835b31

Commits on Apr 5, 2023

• Improved the ability of WORD_RULE to handle some arithmetic-bitwise

  Show description for 9fb826a
  jrh13

  committed
  9fb826a

Commits on Feb 27, 2023

• Made a trivial tweak to overload-proof the new words material.

  jrh13

  committed
  1a1de6c

• Added a general "reverse b-bit fields" operation generalizing the

  Show description for 3de0e70
  jrh13

  committed
  3de0e70

Commits on Jan 18, 2023

• words: extend usimdN to allow returning a word of different size

  aqjune

  committed
  f4b351e

Commits on Nov 18, 2022

• Added some fairly natural notation for SIMD operations on words, as

  Show description for 66cc36b
  jrh13

  committed
  66cc36b

Commits on Oct 19, 2022

• Added material on extended projective coordinates for

  Show description for 1bf0ddf
  jrh13

  committed
  1bf0ddf

Commits on Sep 15, 2022

• Added a definition of x25519, the curve25519 x-coordinate mapping that

  Show description for 3658da9
  jrh13

  committed
  3658da9

Commits on Aug 1, 2022

• Changed the behaviour of the basic "prove" construct for performing

  Show description for 8822aa4
  jrh13

  committed
  8822aa4

Commits on May 11, 2022

• Added a formalization of the "Goldilocks" curve edwards448, based on Mike

  Show description for 538c62f
  jrh13

  committed
  538c62f

Commits on Apr 23, 2022

• Added an update from Marco Maggesi and Cosimo Perini Brogi to their GL

  Show description for ab57c07
  jrh13

  committed
  ab57c07

Commits on Apr 7, 2022

• Extended and cleaned up the elliptic curve material

  Show description for f25b159
  jrh13

  committed
  f25b159

Commits on Mar 5, 2022

• Added a formalization of curve25519, and Montgomery curves in general,

  Show description for 7794982
  jrh13

  committed
  7794982

Commits on Dec 14, 2021

• Added the other SECG curves defined over prime order fields: secp192k1,

  Show description for fb7d8b7
  jrh13

  committed
  fb7d8b7

Commits on Nov 11, 2021

• Added various word and arithmetic lemmas, in particular some using a

  Show description for 43c4ced
  jrh13

  committed
  43c4ced

Commits on Nov 5, 2021

• Added more classic "Hacker's Delight" material as generic word

  Show description for 593af19
  jrh13

  committed
  593af19

Commits on Nov 3, 2021

• Added a few theorems including some systematic gaps in integer

  Show description for 74560a4
  jrh13

  committed
  74560a4

Commits on Oct 7, 2021

• Added a few more word and arithmetic lemmas:

  Show description for 1148eeb
  jrh13

  committed
  1148eeb

Commits on Oct 6, 2021

• Removed trailing whitespace in many files

  jrh13

  committed
  ea44a4c

Commits on Jul 30, 2021

• Added a few more word lemmas:

  Show description for 6a2d07b
  jrh13

  committed
  6a2d07b

Pagination

Previous

Next