Enhance TypeChecker with exponent rules #1713

mccleeary-galois · 2024-07-29T22:17:43Z

Add (x >= 2, x^a * x^b = x^c => a + b = c) to Numeric.hs. Add (Nat a, a * a^x = a^y => 1 + x = y) to SimpType.hs Add (x >= 2, x^a >= x^b => a >= b) to Numeric.hs Start adding tests for exponent TC checks.

src/Cryptol/TypeCheck/Solver/Numeric.hs

… EQ check in Numeric.hs to work for multiplication of exponents as well. Clean up comments by using K for numeric constants, and move numeric constant checks to as early as possibly in Numeric.hs

tests/issues/issue1489/issue1489.cry

mccleeary-galois temporarily deployed to github-pages July 29, 2024 22:17 — with GitHub Actions Inactive

mccleeary-galois force-pushed the rem/solver-exponents branch from 8408a11 to d2fc379 Compare July 30, 2024 14:53

mccleeary-galois temporarily deployed to github-pages July 30, 2024 14:53 — with GitHub Actions Inactive

Enhance TypeCheck to reason more about exponents.

bb77d9f

Add (x >= 2, x^a * x^b = x^c => a + b = c) to Numeric.hs. Add (Nat a, a * a^x = a^y => 1 + x = y) to SimpType.hs Add (x >= 2, x^a >= x^b => a >= b) to Numeric.hs Start adding tests for exponent TC checks.

mccleeary-galois force-pushed the rem/solver-exponents branch from d2fc379 to bb77d9f Compare July 30, 2024 15:35

mccleeary-galois temporarily deployed to github-pages July 30, 2024 15:35 — with GitHub Actions Inactive

mccleeary-galois requested review from yav and marsella July 30, 2024 15:35

Add (x>=2, x^a = x^b => a = b) rule to Numeric.hs.

681fcd4

mccleeary-galois temporarily deployed to github-pages July 30, 2024 17:40 — with GitHub Actions Inactive

yav requested changes Jul 30, 2024

View reviewed changes

Move (K^a * K^b) => K^(a + b) from Numeric.hs to SimpType.hs to allow…

110a753

… EQ check in Numeric.hs to work for multiplication of exponents as well. Clean up comments by using K for numeric constants, and move numeric constant checks to as early as possibly in Numeric.hs

mccleeary-galois temporarily deployed to github-pages July 30, 2024 19:09 — with GitHub Actions Inactive

mccleeary-galois requested a review from yav July 30, 2024 19:15

mccleeary-galois marked this pull request as ready for review July 30, 2024 20:17

yav approved these changes Jul 30, 2024

View reviewed changes

tests/issues/issue1489/issue1489.cry Show resolved Hide resolved

mccleeary-galois mentioned this pull request Jul 30, 2024

Clean up uses of coerceSize GaloisInc/cryptol-specs#101

Closed

mccleeary-galois merged commit 25423ce into master Jul 30, 2024
48 checks passed

mccleeary-galois deleted the rem/solver-exponents branch July 30, 2024 21:14

sauclovian-g mentioned this pull request Aug 1, 2024

Add rule: (a >= 2, fin a, a ^ x == b ^ y) -> x = y #1392

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Enhance TypeChecker with exponent rules #1713

Enhance TypeChecker with exponent rules #1713

mccleeary-galois commented Jul 29, 2024 •

edited

Loading

Enhance TypeChecker with exponent rules #1713

Enhance TypeChecker with exponent rules #1713

Conversation

mccleeary-galois commented Jul 29, 2024 • edited Loading

mccleeary-galois commented Jul 29, 2024 •

edited

Loading