From 23fa15968bd4e5ed29a7bcbdbdbdc7ed82bfbb47 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Thu, 28 Mar 2024 06:42:26 -0400 Subject: [PATCH] remove nonexistent lemma from tutorial --- src/tutorial/properties.md | 36 +++++++++++++++++++++++------------- src/tutorial/sources.rs | 4 ++-- 2 files changed, 25 insertions(+), 15 deletions(-) diff --git a/src/tutorial/properties.md b/src/tutorial/properties.md index 7786061..14b671c 100644 --- a/src/tutorial/properties.md +++ b/src/tutorial/properties.md @@ -5,32 +5,34 @@ panic freedom. After adding a precondition, the signature of the `square` function was `x:u8 -> Pure u8 (requires x <. 16uy) (ensures fun _ -> True)`. This contract stipulates that, given a small input, the function will -*return a value*: it will not panic or diverge. We could enrich the +_return a value_: it will not panic or diverge. We could enrich the contract of `square` with a post-condition about the fact it is a increasing function: ```rust,noplaypen {{#include sources.rs:square_ensures}} ``` + ```ocaml {{#include Sources.fst:square_ensures}} ``` -Such a simple post-condition is automatically proven by F*. The +Such a simple post-condition is automatically proven by F\*. The properties of our `square` function are not fasinating. Let's study a more interesting example: [Barrett reduction](https://en.wikipedia.org/wiki/Barrett_reduction). ## A concrete example of contract: Barrett reduction + While the correctness of `square` is obvious, the Barrett reduction is -not. +not. Given `value` a field element (a `i32` whose absolute value is at most `BARRET_R`), the function `barrett_reduce` defined below computes `result` such that: - - `result ≡ value (mod FIELD_MODULUS)`; - - the absolute value of `result` is bound as follows: - `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)`. +- `result ≡ value (mod FIELD_MODULUS)`; +- the absolute value of `result` is bound as follows: + `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)`. It is easy to write this contract directly as `hax::requires` and `hax::ensures` annotations, as shown in the snippet below. @@ -38,18 +40,26 @@ It is easy to write this contract directly as `hax::requires` and ```rust,noplaypen {{#include sources.rs:barrett}} ``` + ```ocaml {{#include Sources.fst:barrett}} ``` -Note that we call to `cancel_mul_mod`, a lemma: in Rust, this have no + + +Before returning, a lemma may have to be called in F* to prove the correctness +of the reduction. +The lemma is `Math.Lemmas.cancel_mul_mod (v quotient) 3329;`, which establishes +that `(quotient * 3329) % 3329` is zero. +With the help of that one lemma, F\* is able to prove the reduction computes the expected result. +(We may expose lemmas like this to call from Rust directly in future.) This Barrett reduction examples is taken from [libcrux](https://github.com/cryspen/libcrux/tree/main)'s proof of -Kyber which is using hax and F*. +Kyber which is using hax and F\*. This example showcases an **intrinsic proof**: the function `barrett_reduce` not only computes a value, but it also ship a proof @@ -58,6 +68,7 @@ gives the function a formal specification, which is useful both for further formal verification and for documentation purposes. ## Extrinsic properties with lemmas + Consider the `encrypt` and `decrypt` functions below. Those functions have no precondition, don't have particularly interesting properties individually. However, the compostion of the two yields an useful @@ -65,10 +76,10 @@ property: encrypting a ciphertext and decrypting the result with a same key produces the ciphertext again. `|c| decrypt(c, key)` is the inverse of `|p| encrypt(p, key)`. - ```rust,noplaypen {{#include sources.rs:encrypt_decrypt}} ``` + ```ocaml {{#include Sources.fst:encrypt_decrypt}} ``` @@ -77,7 +88,7 @@ In this situation, adding a pre- or a post-condition to either `encrypt` or `decrypt` is not useful: we want to state our inverse property about both of them. Better, we want this property to be stated directly in Rust: just as with pre and post-conditions, the -Rust souces should clearly state what is to be proven. +Rust souces should clearly state what is to be proven. To this end, Hax provides a macro `lemma`. Below, the Rust function `encrypt_decrypt_identity` takes a key and a plaintext, and then @@ -89,8 +100,7 @@ assistant. ```rust,noplaypen {{#include sources.rs:encrypt_decrypt_identity}} ``` + ```ocaml {{#include Sources.fst:encrypt_decrypt_identity}} ``` - - diff --git a/src/tutorial/sources.rs b/src/tutorial/sources.rs index 2cdb102..ad12acd 100644 --- a/src/tutorial/sources.rs +++ b/src/tutorial/sources.rs @@ -50,8 +50,8 @@ fn barrett_reduce(value: i32) -> i32 { let sub = quotient * FIELD_MODULUS; - // Calls a lemma to prove that `(quotient * 3329) % 3329 = 0` - math::lemmas::cancel_mul_mod(quotient, 3329); + // Here a lemma to prove that `(quotient * 3329) % 3329 = 0` + // may have to be called in F*. value - sub }