Skip to content

Instantly share code, notes, and snippets.

@graydon
Created Apr 22, 2018
Embed
What would you like to do?
open FStar.Char
open FStar.Seq
(* Helper *)
let max a b = if a > b then a else b
(* Definition *)
let leftpad (c:char) (n:nat) (s:seq char) : seq char =
let pad = max (n - length s) 0 in
append (create pad c) s
(* Spec and verification *)
let leftpad_correct (c:char) (n:nat) (s:seq char) =
let r = leftpad c n s in
(* Two abbreviations to make conditions more legible *)
let ssz = length s in
let pad = max (n - ssz) 0 in
(* These are all statically discharged *)
let _ = assert (length r = max n ssz) in
let _ = assert (forall (i:nat). i < n - ssz ==> index r i = c) in
let _ = assert (forall (i:nat). i < ssz ==> index r (pad + i) = index s i) in
()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment